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 ingredients:

• A universe Type with Type : Type.
• Dependent products written as forall (x : T₁), T₂ or ∀ (x : T₁), T₂ or ∏ (x : T₁), T₂.
• Dependent sums written as exists (x : T₁), T₂ or Σ (x : T₁), T₂.
• Functions written as fun (x : T) => e or λ (x : T) ⇒ e. The typing annotation may be omitted.
• Application written as e₁ e₂.
• Pairs written as (e₁, e₂)
• First projection written as fst e.
• Second projection written as snd e.
• Type ascription written as e : T.
• Natural numbers type nat : Type with zero and succ n.
• Eliminator for the natural numbers used as match expr with zero -> e₁ | succ m -> e₂.

Top-level commands:

• Definition x := e. -- define a value
• Axiom x : T. -- assume a constant x of type T
• Check e. -- print the type of e
• Eval e. -- evaluate e a la call-by-value
• Load "⟨file⟩". -- load a file

Prerequisites

• OCaml and OPAM

• The OPAM packages menhir and sedlex:

    opam install menhir
    opam install sedlex
  

• It is recommended that you also install the rlwrap or ledit command line wrapper.

Compilation

You can type:

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

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:

• syntax.ml -- abstract syntax of the input
• context.ml -- contexts
• equal.ml -- normalization
• 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
• lexer.ml and 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 unit, bool and nat.