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.
The general problem of 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 by augmenting ML with type annotations or other features.
We present a new proposal, with different goals to much of the existing literature. Our aim is to design a minimal extension to ML to support first-class polymorphism. We err on the side of explicitness over parsimony, extending ML with two new features. First, λ- and let-bindings may be annotated with arbitrary System F types. Second, variable occurrences may be frozen, explicitly disabling instantiation. The resulting language is not always as concise as more sophisticated systems, but in practice it does not appear to require a great deal more ink. FreezeML is a conservative extension of ML, equipped with type-preserving translations back and forth between System F. It admits a type inference algorithm, a mild extension of algorithm W, that is sound and complete and which yields principal types.
Thu 22 Aug (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
|11:20 - 11:45|
Frank EmrichThe University of Edinburgh, Sam LindleyThe University of Edinburgh and Imperial College London, Jan StolarekUniversity of Edinburgh, UK, James CheneyUniversity of Edinburgh, UKPre-print