Typechecker Zoo

Summary

This is a pet project of mine I’ve been working on for a while. We’re going to create minimal implementations of the most successful static type systems of the last 50 years. This will involve making toy implementations of programming languages and the core typechecking algorithms. These obviously have evolved a lot over the years, so we’ll start with the simple ones and proceed all the way up to modern dependent types. Basically a fun romp through half a century of programming language design. We’re going to implement them all in Rust. For no particularly reason, other than it has a decent parser ecosystem and is easy to install. And I like the ironic synthesis of building pure functional languages in a language which is decidedly non-functional. It’s a bit of a heaven-and-hell thing going on, and I’ll leave it up to you to decide on the chirality of that metaphor. This is going to be a more a fun weekend side project, rather than a formal introduction to these systems. If you want authoritative resources read TAPL, ATTAPL and PFPL for the theory and proofs. And also read the primary sources for each typechecker which are linked in the appendix. While the textbooks and papers are great they often focus on the theory in depth and don’t cover the gritty implementation of how to actualy code these kind of typecheckers in real code. In terms of how to lay out the data structures, logic, abstract syntax trees, etc. So we’re going for fun implementation of the gory details of these systems that could be done in a weekend. The examples are implemented in fairly idiomatic Rust with a full parser and test suite, using the usual compiler libraries such as larlpop, logos, ariadne, etc. They are obviously simplified and code golfed versions of the full implementations so that they can be easily understood and modified. But they should be a LOT easier to understand than trying to read production implementations. Parsing is also a solved problem, and MLIR exists so I’m not reall...