FreezeML: complete and easy type inference for first-class polymorphism

Frank Emrich; Sam Lindley; Jan Stolarek; James Cheney; Jonathan Coates

doi:10.1145/3385412.3386003

FreezeML: complete and easy type inference for first-class polymorphism

Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, Jonathan Coates

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

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	https://doi.org/10.1145/3385412.3386003
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	https://conf.researchr.org/home/pldi-2020

Keywords / Materials (for Non-textual outputs)

first-class polymorphism
type inference
impredicative types

Access to Document

10.1145/3385412.3386003Licence: All Rights Reserved

FreezeML_EMRICH_DOA21022020_AFVAccepted author manuscript, 718 KB

https://dl.acm.org/doi/10.1145/3385412.3386003Licence: All Rights Reserved

3 Finished

Turing Fellowship
Cheney, J. (Principal Investigator)
UK-based charities
1/09/18 → 31/08/20
Project: Research
Skye-A programming language bridging theory and practice for scientific data curation
Cheney, J. (Principal Investigator)
EU government bodies
1/09/16 → 28/02/23
Project: Research
From Data Types to Session Types - A Basis for Concurrency and Distribution
Wadler, P. (Principal Investigator)
EPSRC
20/05/13 → 19/11/20
Project: Research

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 Access
File

Cite this

@inproceedings{6b30727099a2454c8383a660d8ac4ecb,

title = "FreezeML: complete and easy type inference for first-class polymorphism",

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.",

keywords = "first-class polymorphism, type inference, impredicative types",

author = "Frank Emrich and Sam Lindley and Jan Stolarek and James Cheney and Jonathan Coates",

year = "2020",

month = jun,

day = "11",

doi = "10.1145/3385412.3386003",

language = "English",

pages = "423--437",

booktitle = "Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

note = "41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020 ; Conference date: 15-06-2020 Through 20-06-2020",

url = "https://conf.researchr.org/home/pldi-2020",

}

Emrich, F, Lindley, S, Stolarek, J, Cheney, J & Coates, J 2020, FreezeML: complete and easy type inference for first-class polymorphism. in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery (ACM), pp. 423-437, 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, London, United Kingdom, 15/06/20. https://doi.org/10.1145/3385412.3386003

FreezeML: complete and easy type inference for first-class polymorphism. / Emrich, Frank; Lindley, Sam; Stolarek, Jan et al.
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery (ACM), 2020. p. 423-437.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - FreezeML

T2 - 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

AU - Emrich, Frank

AU - Lindley, Sam

AU - Stolarek, Jan

AU - Cheney, James

AU - Coates, Jonathan

N1 - Conference code: 41

PY - 2020/6/11

Y1 - 2020/6/11

N2 - 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.

AB - 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.

KW - first-class polymorphism

KW - type inference

KW - impredicative types

U2 - 10.1145/3385412.3386003

DO - 10.1145/3385412.3386003

M3 - Conference contribution

SP - 423

EP - 437

BT - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation

PB - Association for Computing Machinery (ACM)

Y2 - 15 June 2020 through 20 June 2020

ER -

FreezeML: complete and easy type inference for first-class polymorphism

Abstract

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

Turing Fellowship

Skye-A programming language bridging theory and practice for scientific data curation

From Data Types to Session Types - A Basis for Concurrency and Distribution

Research output

Constraint-based type inference for FreezeML

Cite this