Notes on Implementing Algebraic Subtyping

submited by

Style Pass

2024-05-12 07:30:03

Algebraic Subtyping is a type system devised by Stephen Dolan in 2016, in his dissertation. It extends Hindley-Milner with subtyping, in a way that preserves decidability and principality. Over the past few years, I have implemented Algebraic Subtyping in my language Pinafore (omitting record types). Pinafore is, as far as I know, currently the only language to implement this type system besides Dolan’s own MLsub prototype.

These notes are mostly things I wish I knew when writing it. Not having a strong background in type theory, I did not necessarily understand every part of Dolan’s paper before implementing it, but just started work as I understood it. I have learnt a lot since then.

When people interpret and understand the world, we use types, and we make wide use of subtype relations. “X is a dog”, “Y is a cat”, “Z is an animal”, and then, “every cat is an animal”, and so forth. That’s a subtype relation. And you might think that covariance and contravariance are esoteric type-theory concepts, but it turns out that they too are reflected in language: covariance with the word “of” (a bowl of apples is a bowl of fruit), and contravariance with the word “for” (a bowl for fruit is a bowl for apples). It’s therefore helpful to bring these concepts that are already intuitive into the formal type system of a programming language. For example, every text document is a document, every check box is a UI widget, etc.

So of course “object-oriented” languages such as C++, C#, Java, and so forth already have subtyping. However, the type systems of these languages are marred by extraneous complexity. They are not elegant when considered abstractly, making them difficult to reason about. For example, they typically separate “primitive” and “reference” types that behave differently in certain ways; the unit type void is often not a first-class type; type polymorphism is often rather ad-hoc; and there’s no account of contravariance and covariance of type constructors. And the concept of function types tends to be particularly poorly implemented.