Constraint-based type inference for FreezeML

TL;DR

This paper introduces a constraint-based type inference algorithm for FreezeML, a polymorphic type system, modernizing it by enabling the expression of inference problems as constraints and providing a deterministic solving method.

Contribution

It presents the first constraint-based type inference algorithm for FreezeML, including a new constraint language and a deterministic stack machine for solving constraints.

Findings

Proved the termination and correctness of the constraint solving algorithm.

Enabled expression of FreezeML inference problems as constraints.

Extended FreezeML with modern constraint-based inference techniques.

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.