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 $\textsf{let}$-bindings $\textsf{let } x = e_1 \textsf{ in } e_2$ in a fixed order—type $e_1$, generalize its type, and then type $e_2$. 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.
Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | |||
11:00 22mTalk | Decoupling Resolution from Type Inference WITS Lionel Parreaux Hong Kong University of Science and Technology | ||
11:22 22mTalk | First-Class Refinement Types in Scala WITS Matt Bovel EPFL | ||
11:45 22mTalk | Types as grammars WITS Gil Silva LASIGE, University of Lisbon, Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Diana Costa LASIGE, University of Lisbon, Andreia Mordido University of Lisbon, Diogo Poças Instituto de Telecomunicações, University of Lisbon, Vasco T. Vasconcelos LASIGE, University of Lisbon | ||
12:07 22mTalk | Omnidirectional type inference for ML WITS Alistair O'Brien University of Cambridge, Didier Rémy Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS | ||