Omnidirectional type inference for ML: principality any way

TL;DR

This work tackles the fragility of principality in ML-like type systems when faced with features such as static overloading and semi-explicit polymorphism. It introduces omnidirectional type inference, a dynamic constraint-solving framework that suspends constraints when needed and resumes as information becomes available, together with incremental instantiation to refine type schemes during let-generalization. The OmniML calculus formalizes this approach with a constraint language for suspended constraints, a non-deterministic constraint solver, and an efficient implementation plan, proving soundness, completeness, and principality for the targeted features. By applying the framework to OCaml's static overloading and polymorphic methods, the paper demonstrates principled, more expressive type inference than the language's current checker, suggesting broad applicability to other fragile ML extensions and guiding future integration into ML-type systems.

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. 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 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 (let x = e1 in e2) in a fixed order: type e1, generalize its type, and then type e2. 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.