Constraint-based type inference for FreezeML

Frank Emrich, Jan Stolarek, James Cheney, Sam Lindley

Research output: Working paperPreprint

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

Keywords

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

Cite this