FreezeML: Complete and Easy Type Inference for First-Class Polymorphism
| Autor: | Emrich, Frank, Lindley, Sam, Stolarek, Jan, Cheney, James, Coates, Jonathan |
|---|---|
| Rok vydání: | 2020 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| DOI: | 10.1145/3385412.3386003 |
| Popis: | 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. Comment: 48 pages, 23 Figures. Accepted for PLDI 2020 |
| Databáze: | arXiv |
| Externí odkaz: |
|