Typechecker Zoo
As a fun side project, I've built four literate Rust implementations spanning 50 years of type theory research, from Milner's Algorithm W to modern dependent type systems. I've tried to make each implementation as readable and understandable as possible, with detailed explanations and comments throughout the code and to make it as succinct and short as possible so you can pull it into your own projects as a place to start when building any type of system somewhere on the lambda cube.
-Since it's a zoo, I've also given each one a cute animal mascot to represent them:
 |
Algorithm W (Hindley-Milner Type System) Implements Milner's 1978 unification-based type inference using structural recursion. The algorithm generates constraints between type variables during expression traversal, then solves these constraints through Robinson's unification algorithm. Features let-polymorphism enabling rank-1 polymorphic type inference without explicit type annotations. The implementation demonstrates classical occurs check handling and substitution propagation through type environments. Reference: A Theory of Type Polymorphism in Programming by Robin Milner. |
 |
System F (Second-Order Lambda Calculus) Second-order lambda calculus with parametric polymorphism using bidirectional type checking. Bidirectional type checker implementing Dunfield-Krishnaswami algorithm for System F with universal quantification. Splits type checking into synthesis (⇒) and checking (⇐) modes, enabling polymorphic type inference with existential variable solving. Handles parametric polymorphism through universal types (∀α. τ), with careful context management for type variable scoping. Includes comprehensive constraint solving for existential variables and subtyping relations between polymorphic types. Reference: Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism by Dunfield and Krishnaswami. |
 |
System F-ω (Higher-Kinded Polymorphism) A miniature Haskell-lite. Extends System F with type constructors and kind checking, implementing higher-rank polymorphism with algebraic data types. Features kind inference alongside type inference, managing both type-level and kind-level environments. Supports type constructor application and polymorphic kind assignments. Implements constraint generation for higher-kinded unification problems, demonstrating how kind systems prevent malformed type applications. Complete implementation of System F-ω with higher-kinded types, DK bidirectional type checking, existential type variables, polymorphic constructor applications, pattern matching, and lambda expressions with type inference. Reference: A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference by Joshua Dunfield. |
 |
Calculus of Constructions (Dependent Types) The Calculus of Constructions with a hierarchy of non-cumulative universes and inductive types. Full dependent type system unifying types and terms, implementing universe polymorphism with constraint-based inference. Has inductive type definitions, dependent function types (Pi-types, Sigma-types), and universe polymorphism. Uses meta-variable solving for partial solving of higher-order unification problems using Miller pattern technique. Reference: A universe polymorphic type system by Vladimir Voevodsky. |
The examples are implemented in fairly idiomatic Rust with a full parse and test suite (though no evaluator), using the usual compiler libraries such as larlpop, logos, ariande, 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 that trying to read the Haskell or Coq typecheckers which are easily 100k+ LOC each. Hopefully useful to any young, budding language enthusiasts out there. I wish I had had this when I was learning these topics a decade ago so I figured I'd build the resources I would want so that others don't have to struggle so much!