paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Omnidirectional type inference for ML: principality any way

ML 的全向类型推断:无论如何保持主类型性
TOPLAS ACM Transactions on Programming Languages and Systems2026匹配度 2/10 · 该论文属于传统编程语言类型系统与类型推断,虽与静态分析基础有间接关联,但未涉及用户核心关注的 PL 与 AI/LLM/Agent 交叉、浮点程序分析或贝叶斯程序分析,也不是面向工业落地或 benchmark 的问题驱动研究。引用 1 inbox
Alistair O'Brien, Didier Rémy, Gabriel Scherer
crossref: 2026-10-02

AI 速览

一句话:提出全向类型推断,通过可挂起约束与增量实例化在 let-泛化下恢复 ML 扩展的主类型性。

ML 的主类型性保证良类型表达式有唯一最一般类型,但 GADTs、高阶多态和静态重载等扩展引入脆弱构造,破坏主类型性。现有定向推断按固定顺序传播已知类型信息来消歧,却常拒绝本可良类型的程序。本文提出全向类型推断,让类型信息按动态顺序流动:约束可任意顺序求解,信息不足时挂起匹配约束,待信息可用后恢复。为扩展到 ML,作者引入增量实例化,允许实例化含挂起约束的部分类型方案,并随方案精化增量更新实例。该框架在 OCaml 的静态重载(记录标签与数据构造器)和半显式一等多态上得到演示,所得主类型推断算法比 OCaml 当前类型检查器更具表达力。

问题
研究问题:ML 的主类型性在 GADTs、高阶多态、静态重载等扩展下十分脆弱;按固定顺序传播类型信息的定向推断会拒绝一些本可良类型的程序。
方法
提出全向类型推断:约束可任意顺序求解,必要时挂起匹配约束、待信息可用后恢复;并引入增量实例化以支持 let-泛化的任意顺序处理,可实例化含挂起约束的部分类型方案并随方案精化更新实例。
评估
在 OCaml 的静态重载(记录标签与数据构造器)和半显式一等多态两个特性上演示,均获得比 OCaml 当前类型检查器更具表达力的主类型推断算法。
原文摘要(Abstract)

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. Yet, principality is fragile : many extensions of ML—GADTs, higher-rank polymorphism, and static overloading—break it by introducing fragile constructs that resist principal inference. Existing approaches recover principality through directional inference algorithms, which propagate known type information in a fixed (or static ) order ( e.g. as in bidirectional typing) to disambiguate such constructs. However, the rigidity of a static inference order often causes otherwise well-typed programs to be rejected. We propose omnidirectional type inference, where type information flows in a dynamic order. Typing constraints may be solved in any order, suspending when progress requires known type information and resuming once it becomes available, using suspended match constraints . This approach is straightforward for simply typed systems, but extending it to ML is challenging due to let-generalization . Existing ML inference algorithms type let-bindings in a fixed order—type the let-bound expression first, generalize its type, and then type the let-body. To overcome this, we introduce incremental instantiation , allowing partially solved type schemes containing suspended constraints to be instantiated, with a mechanism to incrementally update instances as the scheme is refined. Omnidirectionality provides a general framework for restoring principality in the presence of fragile features. We demonstrate its versatility on two fundamentally different features of OCaml: static overloading of record labels and datatype constructors and semi-explicit first-class polymorphism. In both cases, we obtain a principal type inference algorithm that is more expressive than OCaml’s current typechecker.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot12169,
  title = {Omnidirectional type inference for ML: principality any way},
  author = {Alistair O'Brien and Didier Rémy and Gabriel Scherer},
  booktitle = {TOPLAS},
  year = {2026},
  doi = {10.1145/3848026}
}