Projects per year
Abstract
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.
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.
Original language | English |
---|---|
Title of host publication | Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation |
Publisher | Association for Computing Machinery (ACM) |
Pages | 423-437 |
Number of pages | 15 |
ISBN (Electronic) | 9781450376136 |
DOIs | |
Publication status | Published - 11 Jun 2020 |
Event | 41st ACM SIGPLAN Conference on Programming Language Design and Implementation - London, United Kingdom Duration: 15 Jun 2020 → 20 Jun 2020 Conference number: 41 https://conf.researchr.org/home/pldi-2020 |
Conference
Conference | 41st ACM SIGPLAN Conference on Programming Language Design and Implementation |
---|---|
Abbreviated title | PLDI 2020 |
Country/Territory | United Kingdom |
City | London |
Period | 15/06/20 → 20/06/20 |
Internet address |
Keywords
- first-class polymorphism
- type inference
- impredicative types
Fingerprint
Dive into the research topics of 'FreezeML: Complete and Easy Type Inference for First-Class Polymorphism'. Together they form a unique fingerprint.Projects
- 3 Finished
-
-
Skye-A programming language bridging theory and practice for scientific data curation
1/09/16 → 31/08/22
Project: Research
-
From Data Types to Session Types - A Basis for Concurrency and Distribution
20/05/13 → 19/11/20
Project: Research
Research output
- 1 Article
-
Constraint-based type inference for FreezeML
Emrich, F., Stolarek, J., Cheney, J. & Lindley, S., 31 Aug 2022, In: Proceedings of the ACM on Programming Languages. 6, ICFP, p. 570-595 111.Research output: Contribution to journal › Article › peer-review
Open AccessFile