Omnidirectional type inference for ML: principality any way
Alistair O'Brien, Didier Rémy, Gabriel Scherer
Damas-Hindley-Milner(ML)类型系统的成功归功于公国,每个类型良好的表达式都有独特的最通用类型。 这使得推理可以预测且高效。 不幸的是,ML的许多扩展(GADTs,更高等级的多态性和静态重载)通过引入抵抗主要推理的_fragile_结构来危及原则性。 现有方法通过定向推理算法恢复公国,该算法以固定(或静态)顺序(例如双向类型)传播_known_type信息,以消歧义此类结构。 然而,静态推理顺序的刚性往往导致其他类型良好的程序被拒绝。 我们提出 _omnidirectional_ 类型推理,其中类型信息以动态顺序流。 键入约束可以按任何顺序解决,当进度需要已知类型信息时暂停,并在可用后恢复,使用 _sspended match 约束。 对于简单的类型系统来说,这种方法很简单,但由于允许的概括,将其扩展到ML具有挑战性。 现有的ML推理算法以固定的顺序键入let-bindings(let x = e1 in e2):类型e1,泛化其类型,然后键入e2。 为了克服这一点,我们引入了 _incremental instantiation_,允许实例化包含暂停约束的部分解决类型方案,并在方案完善时逐步更新实例。 综合性为在脆弱特征下恢复公国提供了一个通用框架。 我们在 OCaml 的两个根本不同的特征上展示了它的多功能性:记录标签和数据类型构造函数的静态重载和半显式一等多态性。 在这两种情况下,我们获得了比 OCaml 当前类型 typechecker 更具表现力的主类型推断算法。
The Damas-Hindley-Milner (ML) type system owes its success to principality, the property that every well-typed expression has a unique most general type. This makes inference predictable and efficient. Unfortunately, many extensions of ML (GADTs, higher-rank polymorphism, and static overloading) endanger princpality by introducing _fragile_ constructs that resist principal inference. Existing approaches recover principality through directional inference algorithms, which propagate _known_ type i...