𝐖ell-𝚻yped 𝐑eflections Toggle navigation 𝐖ell-𝚻yped 𝐑eflections<br>Home<br>Archive<br>Categories<br>Tags<br>About
Thoughts on Computer Science & Engineering<br>Lionel Parreaux , Assistant Prof. @ HKUST CSE
Recent Posts<br>Demystifying MLsub — the Simple Essence of Algebraic Subtyping<br>The Y Combinator Explained in Python<br>What is Type Projection in Scala, and Why is it Unsound?<br>Scala Pattern Matching Warts and Improvements<br>Comprehending Monoids with Class
Links<br>I'm looking for PhD students. Apply here!<br>RSS Feed<br>My TACO Lab research group<br>Publications<br>MLscript (nascent programming language)<br>Squid (type-safe metaprogramming for Scala)<br>Github Profile (LPTK)<br>Old Personal Page & Portfolio<br>Twitter Profile<br>Linkedin Profile<br>Curriculum vitae (CV)
Demystifying MLsub — the Simple Essence of Algebraic Subtyping<br>March 26 2020 Note: this web article is an older version of a paper which has now been published as an ICFP Pearl. You can find a preprint of that paper here. It is probably better to read the paper rather than this post , as the paper contains more material, is more up to date, and is better explained!<br>Erratum: A previous version of this article contained a buggy implementation of extrude, which looped when extruding cycling bounds. This was already fixed in the published paper, and the fix has now been ported to the web article.<br>Algebraic subtyping is a new approach to global type inference in the presence of subtyping. It extends traditional Hindley-Milner type inference while preserving the principal type property — that is, it can always infer the most general type for any given expression. This approach was developed by Stephen Dolan as part of his PhD thesis, along with Alan Mycroft.<br>Algebraic subtyping was implemented in the MLsub type inference engine. However, the design of MLsub seems significantly more complex than the simple unification algorithms used for traditional ML languages. MLsub has proven harder to grasp, even for people already familiar with compilers and type systems, such as myself.<br>Dissatisfied with this state of affairs, I wanted to get to the bottom of the algebraic subtyping approach. What really is special about it, beyond the formalism? What are the simple concepts that hide behind the strange notions of biunification and polar types?<br>This article is an answer to those questions. I propose an alternative algorithm for algebraic subtyping, called Simple-sub . Simple-sub can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), and I think it is much more familiar-looking and easier to understand than MLsub.<br>⇨ ⇨ ⇨ You can try Simple-sub online here! ⇦ ⇦ ⇦<br>This article is meant to be light in formalisms and easy to consume for prospective designers of new type systems and programming languages.<br>The complete source code of Simple-sub is available on Github.<br>Summary<br>Introduction
Algebraic Subtyping in MLsub
Algebraic Subtyping in Simple-sub
Simplifying Types
Conclusions
1. Introduction<br>The ML family of languages, which encompasses Standard ML, OCaml, and Haskell, have been designed around a powerful “global” approach to type inference, rooted in the work of Hindley and Milner, later closely formalized by Damas. In this approach, the type system is designed to be simple enough that types can be unambiguously inferred from terms without the help of any type annotations. That is, for any unannotated term, it is always possible to infer a principal type which subsumes all other types that can be assigned to this term. For instance, the term $\lambda{x}. {x}$ can be assigned types $\mathsf{bool} \to \mathsf{bool}$ and $\mathsf{int} \to \mathsf{int}$, but both of these are subsumed by the polymorphic type $\forall a.\ a \to a$, also written 'a -> 'a, which is the principal type of this term.<br>Hindley-Milner (HM) type inference contrasts with more restricted “local” approaches to type inference, found in languages like Scala and C#, which often require the types of variables to be annotated explicitly by programmers. On the flip side, abandoning the principal type property allows these type systems to be more expressive and to support features such as object orientation and first-class polymorphism. Note that in practice, even ML languages like OCaml and Haskell have adopted expressive type system features which, when used, break the principal type property.1<br>Subtyping is an expressive feature allowing types to be structured into hierarchies (usually a subtyping lattice) with the property that types can be refined or widened transparently following this hierarchy. This lets us express the fact that some types are more precise (contain more information) than others, but still have a compatible runtime representation, so that no coercions between them are needed. For instance, in a system where the type nat is a subtype of int, one can transparently use a nat list in place where an int list is expected, without having to apply a coercion function...