An implementation of spartan type theory
This repository shows how to implement a minimalist type theory of the kind that is called "spartan" by some people. The implementation was presented at the School and Workshop on Univalent Mathematics which took place at the University of Birmingham in December 2017. The video recording of the lecture How to implement type theory in an hour is now available.
The type theory
The dependent type theory
spartan has the following ingridients:
- A universe
Type : Type.
- Dependent products written as
forall (x : T₁), T₂or
∀ (x : T₁), T₂or
∏ (x : T₁), T₂.
- Functions written as
fun (x : T) => eor
λ (x : T) ⇒ e. The typing annotation may be omitted.
- Application written as
- Type ascription written as
e : T.
Definition x := e.-- define a value
Axiom x : T.-- assume a constant
Check e.-- print the type of
Eval e.-- evaluate
ea la call-by-value
Load "⟨file⟩".-- load a file
The OPAM packages
opam install menhir opam install sedlex
It is recommended that you also install the
leditcommand line wrapper.
You can type:
maketo make the
make byteto make the bytecode
make cleanto clean up.
make docto generate HTML documentation (see the generated
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 syntax of the input
typecheck.ml-- type checking and conversion from abstract syntax to core type theory
TT.ml-- the core type theory
and continue with the infrastructure
spartan.ml-- interactive top level
print.ml-- printing and message support
desugar.ml-- conversion from parsed syntax to abstract syntax
parser.mly-- parsing into concrete syntax
What experiments should I perform to learn more?
There are many things you can try, for example try adding dependent sums, or basic types