Guarded impredicative polymorphism

Alejandro Serrano, J. Hage, Dimitrios Vytiniotis, Simon Peyton Jones

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The design space for type systems that support impredicative instantiation is extremely complicated. One needs to strike a balance between expressiveness, simplicity for both the end programmer and the type system implementor, and how easily the system can be integrated with other advanced type system concepts. In this paper, we propose a new point in the design space, which we call guarded impredicativity. Its key idea is that impredicative instantiation in an application is allowed for type variables that occur under a type constructor. The resulting type system has a clean declarative specification — making it easy for programmers to predict what will type and what will not —, allows for a smooth integration with GHC’s OutsideIn(X) constraint solving framework, while giving up very little in terms of expressiveness compared to systems like HMF, HML, FPH and MLF. We give a sound and complete inference algorithm, and prove a principal type property for our system.
Original languageEnglish
Title of host publicationProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation
Subtitle of host publicationPLDI 2018
PublisherAssociation for Computing Machinery
Number of pages14
ISBN (Print)9781450356985
Publication statusPublished - 11 Jun 2018


  • Type systems
  • impredicative polymorphism
  • constraint-based inference


Dive into the research topics of 'Guarded impredicative polymorphism'. Together they form a unique fingerprint.

Cite this