A quick look at impredicativity

Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we...

Full description

Saved in:
Bibliographic Details
Published in:Proceedings of ACM on programming languages 2020-08, Vol.4 (ICFP), p.1-29
Main Authors: Serrano, Alejandro, Hage, Jurriaan, Peyton Jones, Simon, Vytiniotis, Dimitrios
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.
ISSN:2475-1421
2475-1421
DOI:10.1145/3408971