Edinburgh Research Explorer

FreezeML: Complete and Easy Type Inference for First-Class Polymorphism

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions

Open

Documents

https://dl.acm.org/doi/10.1145/3385412.3386003
Original languageEnglish
Title of host publicationProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
PublisherAssociation for Computing Machinery (ACM)
Pages423-437
Number of pages15
ISBN (Electronic)9781450376136
DOIs
Publication statusPublished - 11 Jun 2020
Event41st ACM SIGPLAN Conference on Programming Language Design and Implementation - London, United Kingdom
Duration: 15 Jun 202020 Jun 2020
Conference number: 41
https://conf.researchr.org/home/pldi-2020

Conference

Conference41st ACM SIGPLAN Conference on Programming Language Design and Implementation
Abbreviated titlePLDI 2020
CountryUnited Kingdom
CityLondon
Period15/06/2020/06/20
Internet address

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.

    Research areas

  • first-class polymorphism, type inference, impredicative types

Event

41st ACM SIGPLAN Conference on Programming Language Design and Implementation

15/06/2020/06/20

London, United Kingdom

Event: Conference

Download statistics

No data available

ID: 142279779