Types aren’t just annotations for the compiler—they’re a mathematical system that turns out to be the same system as logic. This series works through type theory from the ground up, connecting each idea back to the programming languages you already use. It runs in parallel with Abstract Math for Programmers, and when the two series cover the same concept, they examine it from their respective lens in the same week.

Planned topics

Foundations: What is a type? (base types, type judgments, type safety) — Function types (A → B, lambda abstraction, currying)

Type algebra: Product types (tuples, records) — Sum types (tagged unions, pattern matching) — Void, Unit, and the algebra of types — Cartesian closed categories and the lambda calculus (Lambek’s correspondence)

Polymorphism and abstraction: Type constructors and kinds — Parametric polymorphism (generics, free theorems) — Recursive types and algebraic data types

Logic and effects: The Curry-Howard correspondence (types as propositions, programs as proofs) — Type isomorphisms — Monadic types (Maybe, Either, IO)

Advanced: Dependent types (Π and Σ types) — Substructural types (linear types, Rust’s borrow checker) — Continuations and CPS transforms