A minimalist implementation of type theory in Ocaml. The repository holds several branches which correspond to a series of blog posts about dependent type theory on the Mathematics and Computation blog.
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 thett.native
executable.make byte
to make the bytecodett.byte
executable.make clean
to clean up.make doc
to generate HTML documentation (see the generatedtt.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
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
syntax.ml
-- abstract syntaxcontext.ml
-- contextsnorm.ml
-- normalizationtyping.ml
-- type inference and normalization
and continue with the infrastructure
tt.ml
-- interactive top levelerror.ml
-- error reportingdesugar.ml
-- convert names to de Bruijn indiceslexer.mll
andparser.mly
-- concrete sytnaxbeautify.ml
andprint.ml
-- 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.
There are many things you can try, for example:
- basic types
unit
,bool
andnat
- the eta rule for functions
- dependent sums
- cummulative universes, so that [A : Type k] implies [A : Type (k+1)]
- better type inference so that variables need not be explicitly typed
- prefix and infix operators