2025/11/13 by Alistair O'Brien, O'Brien, Alistair, Didier Rémy +3 · 2 voices
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #cs.PL
paper · pdf · doi:10.48550/arxiv.2511.10343
openalex publication_date 2025/11/13 · openalex created_date 2025/11/15 · openalex updated_date 2026/07/28
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.