Demystifying MLsub – The Simple Essence of Algebraic Subtyping
The article demystifies MLsub, a type system that combines Hindley-Milner type inference with algebraic subtyping. It explains how subtyping can be naturally integrated into a type inference framework using a simple set of typing rules and a union/intersection type structure, allowing for more flexible and expressive type checking without sacrificing principal types or inference.
Background
- Stephen Dolan's PhD work (Cambridge, 2016) that later influenced OCaml. The core problem: traditional type inference (Hindley-Milner, used in OCaml/Haskell) breaks when you add subtyping (passing a specific type where a general one is expected, like Java's `Integer` where `Number` is needed). The solution uses "polarity" — tracking whether a type appears in a "positive" (producing) or "negative" (consuming) position — and a lattice (a mathematical structure of ordered elements) to represent types as sets of constraints.
- MLsub is a research language prototype that implements this theory. The post walks through the math, aiming to make the core insight accessible to programmers who already know type theory. Why it matters: most languages force a choice between automatic type inference (Haskell, SML) or subtyping (Java, C#, Scala). Algebraic Subtyping gives you both, reducing the need for explicit type annotations while keeping flexible, safe subtyping.