Constraint-based type inference for FreezeML

Frank Emrich; Jan Stolarek; James Cheney; Sam Lindley

doi:10.1145/3547642

Constraint-based type inference for FreezeML

Frank Emrich^*, Jan Stolarek, James Cheney, Sam Lindley

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

Abstract

FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was first presented as an extension to Algorithm W. More modern type inference techniques such as HM(X) and OutsideIn(X) employ constraints to support features such as type classes, type families, rows, and other extensions. We take the first step towards modernising FreezeML by presenting a constraint-based type inference algorithm. We introduce a new constraint language, inspired by the Pottier/Rémy presentation of HM(X), in order to allow FreezeML type inference problems to be expressed as constraints. We present a deterministic stack machine for solving FreezeML constraints and prove its termination and correctness.

Original language	English
Article number	111
Pages (from-to)	570-595
Journal	Proceedings of the ACM on Programming Languages
Volume	6
Issue number	ICFP
DOIs	https://doi.org/10.1145/3547642
Publication status	Published - 31 Aug 2022
Event	The 27th ACM SIGPLAN International Conference on Functional Programming, 2022 - Ljubljana, Slovenia Duration: 11 Sept 2022 → 16 Sept 2022 Conference number: 27 https://icfp22.sigplan.org/

Keywords / Materials (for Non-textual outputs)

first-class polymorphism
type inference
impredicative types
constraints

Access to Document

10.1145/3547642Licence: Creative Commons: Attribution (CC-BY)

Constraint-Based_EMRICH_DOA30062022_VOR_CC-BYFinal published version, 333 KBLicence: Creative Commons: Attribution (CC-BY)

https://dl.acm.org/doi/10.1145/3547642Licence: Creative Commons: Attribution (CC-BY)

2 Finished

Effect Handler Oriented Programming
Lindley, S. (Principal Investigator)
MRC
1/02/21 → 31/01/25
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

1 Conference contribution

FreezeML: complete and easy type inference for first-class polymorphism
Emrich, F., Lindley, S., Stolarek, J., Cheney, J. & Coates, J., 11 Jun 2020, Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery (ACM), p. 423-437 15 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Open Access
File

Cite this

@article{16d86b98a6464d2795380efbc56d11c1,

title = "Constraint-based type inference for FreezeML",

abstract = "FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was first presented as an extension to Algorithm W. More modern type inference techniques such as HM(X) and OutsideIn(X) employ constraints to support features such as type classes, type families, rows, and other extensions. We take the first step towards modernising FreezeML by presenting a constraint-based type inference algorithm. We introduce a new constraint language, inspired by the Pottier/R{\'e}my presentation of HM(X), in order to allow FreezeML type inference problems to be expressed as constraints. We present a deterministic stack machine for solving FreezeML constraints and prove its termination and correctness.",

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

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

note = "Funding Information: This work was supported by ERC Consolidator Grant Skye (grant number 682315) and by an ISCF Metrology Fellowship grant provided by the UK government's Department for Business, Energy and Industrial Strategy (BEIS). Lindley is supported by UKRI Future Leaders Fellowship {"}Effect Handler Oriented Programming{"} (MR/T043830/1). Publisher Copyright: {\textcopyright} 2022 Owner/Author.; The 27th ACM SIGPLAN International Conference on Functional Programming, 2022, ICFP 2022 ; Conference date: 11-09-2022 Through 16-09-2022",

year = "2022",

month = aug,

day = "31",

doi = "10.1145/3547642",

language = "English",

volume = "6",

pages = "570--595",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "ICFP",

url = "https://icfp22.sigplan.org/",

}

TY - JOUR

T1 - Constraint-based type inference for FreezeML

AU - Emrich, Frank

AU - Stolarek, Jan

AU - Cheney, James

AU - Lindley, Sam

N1 - Conference code: 27

PY - 2022/8/31

Y1 - 2022/8/31

N2 - FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was first presented as an extension to Algorithm W. More modern type inference techniques such as HM(X) and OutsideIn(X) employ constraints to support features such as type classes, type families, rows, and other extensions. We take the first step towards modernising FreezeML by presenting a constraint-based type inference algorithm. We introduce a new constraint language, inspired by the Pottier/Rémy presentation of HM(X), in order to allow FreezeML type inference problems to be expressed as constraints. We present a deterministic stack machine for solving FreezeML constraints and prove its termination and correctness.

AB - FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was first presented as an extension to Algorithm W. More modern type inference techniques such as HM(X) and OutsideIn(X) employ constraints to support features such as type classes, type families, rows, and other extensions. We take the first step towards modernising FreezeML by presenting a constraint-based type inference algorithm. We introduce a new constraint language, inspired by the Pottier/Rémy presentation of HM(X), in order to allow FreezeML type inference problems to be expressed as constraints. We present a deterministic stack machine for solving FreezeML constraints and prove its termination and correctness.

KW - first-class polymorphism

KW - type inference

KW - impredicative types

KW - constraints

U2 - 10.1145/3547642

DO - 10.1145/3547642

M3 - Article

SN - 2475-1421

VL - 6

SP - 570

EP - 595

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - ICFP

M1 - 111

T2 - The 27th ACM SIGPLAN International Conference on Functional Programming, 2022

Y2 - 11 September 2022 through 16 September 2022

ER -

Constraint-based type inference for FreezeML

Abstract

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

Effect Handler Oriented Programming

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

Research output

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

Cite this