An exploration of Lambda Calculus, programming language design, and type theory starting from a foundation of Bidirectional Typechecking and Normalization by Evaluation.
The foundation series sets the stage with a cohesive STLC implementation we
can build on. The feature museum then grafts on a variety of popular language
features. program and proof build up System Fomega and MLTT based systems
respectively.
Every module is a standalone executable written in a direct style of Haskell with tests. We skip parsing for brevity but include pretty printers from the concrete syntax to a human readable notation to make the examples easier to read.
Each section will eventually conclude with a capstone project implementing a full language including parsing and a repl.
The goal is to provide best practices examples of all the features you might want to include in your custom language in one place.
- Foundation
- Simply Typed Evaluation
- Bidirectional Typechecking
- Normalization By Evaluation
- Elaboration
- Typed Holes
- First Order Unification
- Feature Museum
- Subtyping
- System T
- Records
- Nominal Inductive Types
- Iso-Inductive Types
- Recursion Principles
- Row Polymorphism
- Linear Types
- Modules
- Program
- System F
- System Omega
- System Fomega
- Nominal Recursion
- First Order Unification up to definitional equality
- Implicits
- View Patterns
- Proof
- Martin-Lof Type Theory
- Type Universes
- Universe Polymorphism
- Indexed Inductive Types (with eliminators)
- Dependent Pattern Matching
- Case-Trees
- Termination / Coverage Checking
- Implicit Universe Levels with Constraint Solving
- Tarski Universes
- Dependent View Patterns
- Cubical
Additionally we plan to provide complete examples of STLC, SystemF, and MLTT compiling to the following targets:
- Javascript
- A simple stack machine
- LLVM
The ultimate goal is build a 1lab style literate coded webapp that allows exploring Lambda Calculus in all its forms.