FreezeML: Complete and Easy Type Inference for First-Class Polymorphism
ML is remarkable in providing statically typed polymorphism without the
programmer ever having to write any type annotations.
The cost of this parsimony is that the programmer is limited to a form of
polymorphism in which quantifiers can occur only at the outermost level of a
type and type variables can be instantiated only with monomorphic types.
Type inference for unrestricted System F-style
polymorphism is undecidable in general. Nevertheless, the literature abounds
with a range of proposals to bridge the gap between ML and System F.
We put forth a new proposal, FreezeML, a conservative extension of ML with two
new features. First, let- and lambda-binders may be annotated with arbitrary
System F types. Second, variable occurrences may be frozen, explicitly
disabling instantiation. FreezeML is equipped with type-preserving
translations back and forth between System F and admits a type inference
algorithm, an extension of algorithm W, that is sound and complete and which
yields principal types.
Thu 18 JunDisplayed time zone: Pacific Time (US & Canada) change
09:20 - 10:20 | Type SystemsPLDI Research Papers at PLDI Research Papers live stream Chair(s): Arjun Guha Northeastern University | ||
09:20 20mTalk | Predictable Accelerator Design with Time-Sensitive Affine Types PLDI Research Papers Rachit Nigam Cornell University, USA, Sachille Atapattu Cornell University, USA, Samuel Thomas Cornell University, USA, Zhijing Li Cornell University, USA, Theodore Bauer Cornell University, USA, Yuwei Ye Cornell University, USA, Apurva Koti Cornell University, USA, Adrian Sampson Cornell University, USA, Zhiru Zhang Cornell University, USA | ||
09:40 20mTalk | Type-Directed Scheduling of Streaming Accelerators PLDI Research Papers David Durst Stanford University, USA, Matthew Feldman Stanford University, USA, Dillon Huff Stanford University, USA, David Akeley University of California at Los Angeles, USA, Ross Daly Stanford University, USA, Gilbert Bernstein University of California at Berkeley, USA, Marco Patrignani Stanford University, USA / CISPA, Germany, Kayvon Fatahalian Stanford University, USA, Pat Hanrahan Stanford University, USA | ||
10:00 20mTalk | FreezeML: Complete and Easy Type Inference for First-Class Polymorphism PLDI Research Papers Frank Emrich University of Edinburgh, UK, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK / Imperial College London, UK, Jan Stolarek University of Edinburgh, UK, James Cheney University of Edinburgh, UK, Jonathan Coates University of Edinburgh, UK | ||