elab-dependent

A small dependently typed language

This is an implementation of a small dependently typed language where types are first-class and where the return type of a function may depend on the arguments it is applied to.

Type checking is is implemented in terms of an elaborator, which checks and tanslates a user-friendly surface language into a simpler and more explicit core language that is more closely connected to type theory. Because we need to simplify types during elaboration we also implement an interpreter for the core language.

This was originally posted at tt-hoas-nameless.ml.

Example

let Bool : Type := fun (Out : Type) (true : Out) (false : Out) -> Out;
let true : Bool := fun Out true false => true;
let false : Bool := fun Out true false => false;

let not : Bool -> Bool := fun b =>
  fun Out true false => b Out false true;

true Bool false

$ cat ./test/readme/bools.txt | dependent norm
<input> :
  fun (false : fun (Out : Type) (true : Out) (false : Out) -> Out)
      (Out : Type) (true : Out) (false : Out) -> Out
:= fun false Out true false := false

Some useful resources

• elaboration-zoo: Some excellent, high quality examples of implementing elaborators for dependently typed programming languages, demonstrating bidirectional type checking and normalisation-by-evaluation, and extensions to this.
• mb64’s excellent gists showing tiny type system implementations:
  • mlt.ml
  • tychk_nbe.ml
• A Tutorial Implementation of a Dependently Typed Lambda Calculus by Andres Löh, Conor McBride and Wouter Swierstra: A little outdated compared to the above implementations, but the paper is still worth a look, showing how to incrementally add dependent types to a simply typed lambda calculus.
• nbe-for-mltt: An implementation of bidirectional typechecking and normalisation-by-evaluation for dependent types. Some more information on the implementation can be found in the paper, Implementing a Modal Dependent Type Theory by Daniel Gratzer, Jonathan Sterling and Lars Berkedal.
• Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Thrane Christiansen: Implements a dependent typechecker using bidirectional type checking and normalisation-by-evaluation.