Fri 22 Jun 2018 16:10 - 16:35 at Grand Ballroom CD - Types Chair(s): Kathleen Fisher

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.

Fri 22 Jun

Displayed time zone: Eastern Time (US & Canada) change

16:10 - 17:25
TypesPLDI Research Papers at Grand Ballroom CD
Chair(s): Kathleen Fisher Tufts University
16:10
25m
Talk
Guarded Impredicative Polymorphism
PLDI Research Papers
Alejandro Serrano Utrecht University, Jurriaan Hage Utrecht University, Dimitrios Vytiniotis Microsoft Research, Cambridge, Simon Peyton Jones Microsoft Research
Media Attached
16:35
25m
Talk
Typed Closure Conversion for the Calculus of Constructions
PLDI Research Papers
William J. Bowman Northeastern University, USA, Amal Ahmed Northeastern University, USA
Media Attached
17:00
25m
Talk
Inferring Type Rules for Syntactic Sugar
PLDI Research Papers
Justin Pombrio Brown University, USA, Shriram Krishnamurthi Brown University, USA
Media Attached