Start with a checker that answers "what type is this?" for literals and end with an inference engine that reads an unannotated program and works out its principal type on its own. Every lesson is one concrete spec: type equality, variable scoping, arrow types, unification, the occurs check that rejects infinite types, generalization so let id = \x.x is polymorphic, and type errors that carry a source location.
Over 36 lessons you build a working type checker for a small functional language, from the ground up. You start with a representation of types (Int, Bool, String) and a tiny expression AST, and write a checker that answers "what type is this?" for literals, variables in a typing environment, let-bindings with lexical scope, explicitly-typed functions and application, and conditionals - a complete, usable checker for explicitly-typed programs.
Then you build the inference core that makes the annotations optional: type variables and fresh names, substitutions you can apply and compose, unification of two types, and the occurs check that rejects infinite types like the one hidden in \x. x x. You wire these into Algorithm W - inferring application, lambdas and conditionals by unification, then generalization and instantiation so that let id = \x.x is polymorphic and works at both Int and Bool, while a lambda-bound parameter stays monomorphic. You finish with richer types - arithmetic operators, recursion, tuples, lists, and records - and quality diagnostics: type errors that name the expected and actual types and point at a source position.
This is a teaching-grade Hindley-Milner checker built around the real Algorithm W design: it infers the principal type of an unannotated program, reports the first type error with a location, and is honest about its edges - it takes a pre-built AST rather than parsing source text, and it reports one type error at a time rather than recovering to collect them all. The capstone infers the principal type of a small polymorphic program and reports the located error in an ill-typed one - the same core that sits inside the type systems of ML, Haskell, and their descendants.
A type checker's whole job is to decide whether two types are the same, so before anything else you need types you can represent and compare. Today you build the three base types and the equality check that every later rule leans on.
Represent the Int, Bool, and String types and decide whether two types are equal.
A type checker is, at heart, a machine that keeps asking one question: are these
two types the same? Is the thing in the then branch the same type as the thing
in the else branch? Is the argument the same type the function expects? Every
rule you write from here reduces to that comparison, so the very first thing to
build is a way to represent a type and a way to compare two of them.
Start with the three base types - Int, Bool, and String - as distinct
values, and a single Equal function that reports whether two types have the same
shape. Right now “same shape” just means “same base type”, but this is the seam the
whole project widens: soon a type can be a function, a tuple, or an unknown to be
discovered, and Equal (and later, unification) will compare those structurally
too. Keep today’s version as simple as it looks.
// a Type is one of a small, growing set of shapes.// Start with the three ground types as distinct values.type Type interface{ typeNode() }type TInt struct{}type TBool struct{}type TString struct{}// Equal answers the one question the checker asks constantly.func Equal(a, b Type) bool { /* same shape? */ }
A complete, correctly-threaded Hindley-Milner core - literals through functions, let-polymorphism, tuples, lists, records, arithmetic and recursion, and located type errors - usable as an importable checker API and demonstrated by a runnable demo, but it types a pre-built AST rather than parsing source text, reports one error at a time with no recovery, and stops short of row polymorphism, type classes, user-defined data types, and modules.
The standard modern text on type systems. The simply-typed lambda calculus and type-reconstruction chapters cover exactly the explicit checker and the unification-based inference this project builds.
The 1982 paper that introduced Algorithm W and proved it finds the principal type. The generalization and instantiation rules in chapter four come straight from here.
Milner 1978 - the origin of let-polymorphism and the unification-based type discipline. The reason let generalizes and a lambda parameter does not.
A famously readable, implementation-oriented walkthrough of a Hindley-Milner checker - unification, the occurs check, generalization - the practical companion to the theory papers.
A hands-on chapter that builds Algorithm W with substitutions and a fresh-variable supply, the same functional design used here, with runnable code to compare against.
The named type discipline this project implements - principal types, let-generalization, and unification-based inference. A good anchor for the vocabulary the lessons use.