Constraint-based type inference for FreezeML

Frank Emrich, Jan Stolarek, James Cheney, Sam Lindley

Research output: Working paperPreprint


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\'emy 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
Number of pages45
Publication statusPublished - 20 Jul 2022


  • first-class polymorphism
  • type inference
  • impredicative types
  • constraints
  • Software and its engineering
  • Polymorphism
  • Functional languages

Cite this