# How to implement dependent type theory II

I am on a roll. In the second post on how to implement dependent type theory we are going to:

1. Spiff up the syntax by allowing more flexible syntax for bindings in functions and products.
2. Keep track of source code locations so that we can report where the error has occurred.
3. Perform normalization by evaluation.

The relevant Github repository is andrejbauer/tt/ (branch blog-part-II). By the way, there are probably bugs in the implementation, I am not spending a huge amount of time on testing (mental note: put “implement testing” on the to do list). If you discover one, please tell me, or preferrably make a pull request with a fix. This also applies to old branches.

### Source code positions

Source code positions seem like an annoyance because they pollute our nice datatypes. Nevertheless, an even bigger annoyance is an error message without an indication of its position.

The OCaml lexer keeps track of positions, and menhir has support for them, so we just need to incorporate them into our program. Every expression should be tagged with the source code position it came from. Sometimes we generate expressions with no associated position, so we define:

type position =
| Position of Lexing.position * Lexing.position
| Nowhere


The type Lexing.position is the one from OCaml lexer. Each expression is associated with two such positions, its beginning and end. To tag expressions with positions we define two types: expr is an expression with a position and expr' without (I stole the idea from Matija Pretnar‘s eff code):

(** Abstract syntax of expressions. *)
type expr = expr' * position
and expr' =
| Var of variable
| Universe of int
| Pi of abstraction
| Lambda of abstraction
| App of expr * expr

(** An abstraction [(x,t,e)] indicates that [x] of type [t] is bound in [e]. *)
and abstraction = variable * expr * expr


Note that expr' refers back to expr so that subexpressions come equipped with their positions. We generally follow the rule that an apostrophe is attached to a type or a function which is position-less. Except that apostrohpies are not valid in the names of grammatical rules in the parser, so in parser.mly we write plain_expr instead of expr'.

We also extend the pretty printer and error reporting with positions, feel free to consult the source code.

### Better syntax for bindings

This is a fairly trivial change. It is annoying to have to write things like

fun x : A => fun y : A => fun z : B => fun w : B => ...


We improve the parser so that it accepts syntax like

fun (x y : A) (z w : B) => ...


Let us read out the relevant portion of parser.mly, namely the rules abstraction, bind1 and binds:

abstraction:
| b = bind1
{ [b] }
| bs = binds
{ bs }

Name

E-mail

Website

Comment