In recent years, there has been increasing interest in tools and programming languages that can automatically detect common types of bugs, in order to improve product quality and programmer productivity. Most commonly, this is done via static type systems, but traditional static type systems require large amounts of manual annotation by programmers, making them difficult to work with. Therefore, modern programming languages make increasing use of type inference, which provides the same benefits with few or no manual type annotations required.
The most popular form of type inference is based on the Hindley-Milner system, which is limited by its lack of support for subtyping. In his 2016 PhD thesis, Stephen Dolan introduced Algebraic Subtyping, a new type inference system with full subtyping support. However, as an academic thesis, Algebraic Subtyping is an intimidating 157 pages full of formal mathematical proofs and short on practical implementation guidance.
As someone who has spent much of the subsequent three and a half years understanding algebraic subtyping and trying to implement it in practical programming languages, I want to share the results of my studies. In this series of blog posts, I will show you how to actually implement algebraic subtyping, or rather, an improved version I call cubic biunification which is faster and easier to understand, with detailed, step-by-step code examples and zero mathematical proofs.
What is subtype inference and why is it important?
Most current languages with type inference use some variation of the Hindley-Milner system, which is based around unification, the process of iteratively equating types to solve constraints. Unfortunately, this results in a system which is inflexible and unintuitive, leading to many language specific hacks and extensions in an attempt to work around the resulting issues.
With unification, values that are used together are forced to have the same type. If you pass a value to a function, it’s not enough for that value to have a type compatible with the function’s argument type. Unification forces it to be equal to the function’s argument type. If you pass two different values to the same function, they are forced to have the same type. Effectively, type constraints are propagated both forwards and backwards relative to the dataflow of your program, which is confusing and leads to many type errors that do not reflect real bugs in the underlying program logic. A number of workarounds have been developed to avoid this issue in specific cases, but the underlying problem persists in any HM-derived inference system.
With subtyping by contrast, type inference is based around ensuring that each value has a type compatible with its usages. Constraints follow the data flow of your program but do not flow “backwards”, so there are no spurious type errors just because you happened to pass two different values with different, but compatible, types in the same place. This makes type inference much more powerful and also more intuitive.
Furthermore, I think that evaluating subtype inference in the context of existing programming languages and paradigms undersells its potential, because it facilitates new styles of programming that are largely unexplored. In particular, most programming languages are reliant on programmer supplied type annotations, which means that each feature in the type system must have corresponding syntax in type annotations and must be easy to write concisely in said syntax. In effect, the type system is limited by the need to maintain a convenient manual type syntax.
The ability to typecheck an entire program with no manual type annotations removes this constraint and means that the programming language designers are free to experiment with new and more sophisticated types of static analysis with no burden on the end user. (Hindley-Milner of course does not require manual type annotations either, but the lack of subtyping makes its use less practical).
For example, the programming language Rust has structurally inferred traits ( Send , Sync , etc.) used to statically ensure properties such as thread safety and unwind safety. By default, a new type in Rust is considered thread safe if all of its components are thread safe and so on, meaning that the safety checks operate largely automatically with only the occasional need for explicit concern from the programmer. The subtype inference system presented here is capable of implementing similar features with minimal changes to the compiler, making it easy to experiment with adding such safety checks with no changes required to the end user code base.
... continue reading