A Quick Look at Impredicativity (ICFP 2020)

Alejandro Serrano presents a practical design for impredicative type inference implemented in GHC.

More info about this talk: icfp20.sigplan.org/details/icfp-2020-papers/18/A-Quick-Look-… Authors: Alejandro Serrano, 47 Degrees, Spain (presenting) Jurriaan HageUtrecht University, Netherlands Simon Peyton Jones, Microsoft, UK Dimitrios Vytiniotis, DeepMind Abstract: 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. This is an official ICFP 2020 talk video edited from an author-submitted video. Video captions supported by Jane Street. On a desktop browser, you can view captions without overlapping the video by clicking the three dots to the right of “Save” and clicking “Open transcript”.