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