Algebraic Subtyping: PhD thesis

Stephen Dolan’s PhD thesis on “Algebraic Subtyping” is now available (comment thread).

Type inference gives programmers the benefit of static, compile-time type checking without the cost of manually specifying types, and has long been a standard feature of functional programming languages. However, it has proven difficult to integrate type inference with subtyping, since the unification engine at the core of classical type inference accepts only equations, not subtyping constraints.

This thesis presents a type system combining ML-style parametric polymorphism and subtyping, with type inference, principal types, and decidable type subsumption. Type inference is based on biunification, an analogue of unification that works with subtyping constraints.

Related Posts

Author | Gemma Gordon

Gemma is the Operations Director for the OCaml Labs group in the Cambridge Computer Laboratory, and covers day-to-day management, investigates funding opportunities and organises events.