The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy

The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy, Lionel Parreaux, ICFP 2020.

MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand.

There's also an introductory blog post and an online demo.

Stephen Dolan's Algebraic Subtyping (discussion) unexpectedly provided a solution to the problem of combining type inference and subtyping, but used somewhat heavy and unusual machinery. Now Lionel Parreaux shows that the system can be implemented in a very straightforward and pleasing way. Here's to hoping that it makes it into real languages!

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Wow

There's a lot to assimilate here. I tackle a bit more of it every day or two, but I can see it's going to be some time before I grok it in fullness. And I do hope to get there, because it really is quite cool. I'm oddly reminded of the Church-Rosser theorem, which was first published in 1936 but the first simple proofs didn't become publicly available for about another three and a half decades. And I say this (not to misrepresent my position) as someone who doubts the advisability of advanced typing in programming languages, and has even stronger doubts about type inference in particular. Even at the height of my enthusiasm-for-powerful-typing phase, I'd never quite felt motivated to study Hindley-Milner in depth, so I'm going to have to play catch-up, here; but it seems well worth it, and you've provided plenty of hooks for the particular work (including the earlier LtU thread, which felt awfully esoteric at the time). And all this clearly relates to the notions of covariance and contravariance, which I've been probing lately as part of my ongoing effort to get a grip on tensors but somehow hadn't connected back to typing. Thanks for this!