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

DevFeed: [The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy](<https://devfeed.tech/articles/the-simple-essence-of-algebraic-subtyping-principal-type-inference-with-subtyping-made-easy-29481.md>)

Original publisher: [Read original article](<http://lambda-the-ultimate.org/node/5597>)

Published: 2020-07-24T07:46:20Z

Content type: article

Language: en

Sources: [Lambda the Ultimate](<https://devfeed.tech/sources/lambda-the-ultimate.md>)

Topics: [Algorithm](<https://devfeed.tech/topics/algorithm.md>), [Code](<https://devfeed.tech/topics/code.md>), [Parser](<https://devfeed.tech/topics/parser.md>), [pretty printing](<https://devfeed.tech/topics/pretty-printing.md>)

Tags: [algorithm](<https://devfeed.tech/tags/algorithm.md>), [blog-post](<https://devfeed.tech/tags/blog-post.md>), [code](<https://devfeed.tech/tags/code.md>), [parsing](<https://devfeed.tech/tags/parsing.md>), [pretty-printing](<https://devfeed.tech/tags/pretty-printing.md>), [type-theory](<https://devfeed.tech/tags/type-theory.md>)

## AI overview

The article presents Simple-sub, an alternative algorithm for algebraic subtyping and principal type inference. It argues that MLsub's biunification-based specification can be understood without bisubstitution, polar types, and advanced abstract algebra, and reports that the implementation fits in under 500 lines of code.

## Source excerpt

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!