Programming Languages and Compilers Commons^™

The Algebra Of Type Unification, Verity James Scheel

Senior Projects Spring 2022

Type unification takes type inference a step further by allowing non-local flow of information. By exposing the algebraic structure of type unification, we obtain even more flexibility as well as clarity in the implementation. In particular, the main contribution is an explicit description of the arithmetic of universe levels and consistency of constraints of universe levels, with hints at how row types and general unification/subsumption can fit into the same framework of constraints. The compositional nature of the algebras involved ensure correctness and reduce arbitrariness: properties such as associativity mean that implementation details of type inference do not leak in …