A cute collection of type checker implementations demonstrating modern type checking algorithms from the last fifty years of programming language design.
 Algorithm W |
 Type Classes |
 System F |
 System F-ω |
 Refinement Types |
 Calculus of Constructions |
 Row Polymorphism |
 Row Effects |
 Call-by-Push-Value |
Robin Milner's classic Hindley-Milner type inference algorithm from A Theory of Type Polymorphism in Programming.
Haskell-style type classes layered on top of Hindley-Milner, with superclasses, default methods, and dictionary-passing elaboration.
Follows the qualified-types presentation from Mark Jones' Typing Haskell in Haskell.
Second-order lambda calculus with parametric polymorphism using bidirectional type checking.
An implementation of bidirectional algorithm from Complete and Easy Bidirectional Typechecking for Higher-rank Polymorphism.
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.
Uses the method of A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference.
A refinement-typed lambda calculus that discharges obligations to Z3 via Rust FFI bindings.
Inspired by the Liquid Types approach of Rondon, Kawaguchi and Jhala.
The Calculus of Constructions with a hierarchy of non-cumulative universes, inductive types and universe polymorphism. Limited support for higher-order unification.
Uses a bidirectional dependent typechecker outlined in A universe polymorphic type system by Vladimir Voevodsky.
Koka-style extensible records with scoped labels: duplicate labels are allowed and shadow on selection.
Inspired by the system from Extensible records with scoped labels by Daan Leijen.
Algebraic effects and handlers using the same scoped-label row machinery.
A lambda calculus separating values from computations which subsumes both call-by-value and call-by-name. Bidirectional typechecker with two judgment forms.
Basic implementation of Levy's Call-by-Push-Value: A Functional/Imperative Synthesis.
Do the Rust (latest stable) install then:
brew install just # or ( cargo install just )
just build # Build all projects
just test # Run all testsThe tutorial is built with mdBook and mdbook-include-rs preprocessor.
just install-docs # Install mdbook and dependencies
just build-docs # Build documentation
just serve-docs # Serve with live reloadIf you want to contribute, please fork the repository and submit a pull request.
# Clone the repository
git clone https://github.com/sdiehl/typechecker-zoo.git
cd typechecker-zoo/docs
# Install mdBook and the include preprocessor
cargo install --git https://github.com/sdiehl/mdbook-include-rs.git
# Start the mdBook preview
just serve-docs
# Make your edits to markdown files in src/Then open a pull request on Github. Any contributions are welcome, especially typo fixes and improvements. 🙏
MIT Licensed. Copyright 2025-2026 Stephen Diehl.