A series of Lambda Calculus implementations starting from Simply Typed evaluation, then work up through bidirectional typechecking, normalization by evaluation, elaboration and various type system extensions.
These examples build up sequentially, but each module is a standalone program that can be read independently. 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.
The goal is to provide best practices examples of all the features you might want to include in your custom language in one place.
- SimplyTypedEvaluation
- BidirectionalTypechecking
- NormalizationByEvaluation
- Elaboration
- TypedHoles
- System T
- Records
- Subtyping
- Nominal Inductive Types
- Iso-Inductive Types
- System F
- Martin-Lof Type Theory (Pi and Sigma Types)
- Type Universes
- Universe Polymorphism
- Unification / Implicits
- Indexed Inductive Types (with eliminators)
- Dependent Patern Matching
- Case-Trees
- Termination / Coverage Checking
- Implicit Universe Levels with Constraint Solving
- Tarski Universes
- Row Polymorphism
- Linear Types
- View Patterns
- Cubical
- Modules
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.