论文标题
基于约束的freezeml推断
Constraint-based type inference for FreezeML
论文作者
论文摘要
Freezeml是一种新的一流多态性推理的方法，它采用术语注释来控制何时以及如何实例化和推广多态性类型。它保守地扩展了Hindley-Milner类型的推理，并首先作为算法W的扩展。更现代的类型推理技术，例如HM（X）和Oxexialin（$ X $）采用限制来支持类型类，类型家庭，行，行和其他扩展等功能。我们通过介绍基于约束的推理算法迈出了现代化的Freezeml的第一步。我们引入了一种新的约束语言，灵感来自HM（X）的Pottier/Rémy演示，以便允许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.
