Lionel Parreaux presents Simple-sub, a simplified algorithm for algebraic subtyping and principal type inference.
The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)
More info about this talk: icfp20.sigplan.org/details/icfp-2020-papers/37/The-Simple-Es…
Author: Lionel Parreaux, EPFL (presenting)
Abstract:
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.
We present an experimental evaluation of Simple-sub against MLsub on a million randomly-generated well-scoped expressions, showing that the two systems agree. The mutable automaton-based implementation of MLsub is quite far from its algebraic specification, leaving a lot of space for errors; in fact, our evaluation uncovered several bugs in it. We sketch more straightforward soundness and completeness arguments for Simple-sub, based on a syntactic specification of the type system.
This paper is meant to be light in formalism, rich in insights, and easy to consume for prospective designers of new type systems and programming languages. In particular, no abstract algebra is inflicted on readers.
This is an official ICFP 2020 talk video edited from an author-submitted video. Video captions supported by Jane Street. On a desktop browser, you can view captions without overlapping the video by clicking the three dots to the right of “Save” and clicking “Open transcript”.
Why it's here
1 person recommends this
What people say. Recommended as a reference for implementing type inference in custom compilers.
g
u/gelisamin r/haskell • Recommends
On “Is there a standardized programming model to build compilers with Haskell that I can follow to assure the best results?”
> Is there a standardized programming model to build compilers with Haskell
Gabriella Gonzles's Fall-from-Grace is intended to be a demonstration of best practices when implementing a language in Haskell. If you were starting a brand new project, I would recommend to fork it and to gradually modify the Grace language into your language, but since you've already started, I recommend to look at the code for inspiration instead.
> So my question is: we already have stateful monads and parsers like parsec as an architectural model to implement the syntax analysis ...
Looking up "syntax analyzis", I see that "Syntax Analysis is a second phase of the compiler design process in which the given…
