一句话：为 FreezeML 提出基于约束的类型推断，借助新约束语言与确定性栈机求解，并证明终止性和正确性。
FreezeML 是一种支持一等多态类型推断的方法，通过项标注控制多态类型的实例化与泛化，此前仅以 Algorithm W 扩展形式给出。为融入 HM(X)、OutsideIn(X) 等现代约束式推断技术，本文首次将 FreezeML 现代化：设计一种受 Pottier/Rémy 的 HM(X) 表述启发的新约束语言，把 FreezeML 类型推断问题编码为约束。论文给出求解这些约束的确定性栈机，并证明该求解器终止且相对于类型系统正确。这为 FreezeML 扩展类型类、类型族、行多态等特性奠定基础。
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.
@article{paperbot1490,
title = {Constraint-based type inference for FreezeML},
author = {Frank Emrich and Jan Stolarek and James Cheney and Sam Lindley},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547642}
}