Constraint-based type inference for FreezeML

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

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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 languageEnglish
Article number111
Pages (from-to)570-595
JournalProceedings of the ACM on Programming Languages
Issue numberICFP
Publication statusPublished - 31 Aug 2022
EventThe 27th ACM SIGPLAN International Conference on Functional Programming, 2022 - Ljubljana, Slovenia
Duration: 11 Sept 202216 Sept 2022
Conference number: 27

Keywords / Materials (for Non-textual outputs)

  • first-class polymorphism
  • type inference
  • impredicative types
  • constraints


Dive into the research topics of 'Constraint-based type inference for FreezeML'. Together they form a unique fingerprint.

Cite this