Skip to content
A minimalist implementation of type theory, suitable for experimentation
OCaml TeX Emacs Lisp Shell Makefile JavaScript Standard ML
Find file
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


A minimalist implementation of type theory in fewer than 500 lines of Ocaml code, including comments. This version corresponds to the one described in the blog post How to implement dependent type theory I.

The type theory

The dependent type theory tt has the following ingridients:

  • The universes are Type 0, Type 1, Type 2, ...
  • A dependent product is written as forall x : T1, T2
  • A function is written as fun x : T => e
  • Application is written as e1 e2

The hierarchy of universes is not commulative, i.e., even though Type k has type Type (k+1), Type k is not a subuniverse of Type (k+1).


You need ocamlbuild, which is part of OCaml, the menhir parser generator, and make. You can type

  • make to make the tt.native executable.
  • make byte to make the bytecode tt.byte executable.
  • make clean to clean up.
  • make doc to generate HTML documentation (see the generated tt.docdir/index.html).


Type Help. in the interactive shell to see what the type system can do. Here is a sample session:

tt blog-part-I
[Type Ctrl-D to exit or "Help." for help.]
# Parameter N : Type 0.
N is assumed
# Parameter z : N. Parameter s : N -> N.
z is assumed
s is assumed
# Definition three := fun f : N -> N => fun x : N => f (f (f x)).
three is defined
# Context.
three = fun f : N -> N => fun x : N => f (f (f x))
    : (N -> N) -> N -> N
s : N -> N
z : N
N : Type 0
# Check (three (three s)).
three (three s)
    : N -> N
# Eval (three (three s)) z.
    = s (s (s (s (s (s (s (s (s z))))))))
    : N

Source code

The purpose of the implementation is to keep the source uncomplicated and short. The essential bits of source code can be found in the following files. It should be possible for you to just read the entire source code. You should start with the core

  • -- abstract syntax
  • -- contexts
  • -- type inference and normalization

and continue with the infrastructure

  • -- interactive top level
  • -- error reporting
  • lexer.mll and parser.mly -- concrete sytnax
  • and -- pretty printing


The code is meant to be short and sweet, and close to how type theory is presented on paper. Therefore, it is not suitable for a real implementation, as it will get horribly inefficient as soon as you try anything complicated. But it should be useful for experimentation.

What experiments should I perform to learn more?

There are many things you can try, for example:

  • basic types unit, bool and nat
  • the eta rule for functions
  • dependent sums
  • de Bruijn indices
  • cummulative universes, so that [A : Type k] implies [A : Type (k+1)]
  • better type inference so that variables need not be explicitly typed
  • flexible syntax, e.g., allow fun x y : nat => ... instead of fun x : nat => fun y : nat => ...
  • prefix and infix operators
Something went wrong with that request. Please try again.