Remarks on implementation

As is common for normalization-by-evaluation, the implementation uses De Bruijn indices for syntactic terms and De Bruijn levels for semantic values. A little more unusually, however, the De Bruijn indices are “intrinsically well-scoped”. This means that the type of terms is parametrized by the length of the context (as a type-level natural number, using GADTs), so that the OCaml compiler ensures statically that De Bruijn indices never go out of scope. Other consistency checks are also ensured statically in a similar way, such as the matching of dimensions for certain types and operators, and scoping and associativity for notations. (The latter is the reason why tightnesses are dyadic rationals: they are represented internally as type-level finite surreal-number sign-sequences, this being a convenient way to inductively define a dense linear order.)

This approach does have the drawback that it requires a fair amount of arithmetic on the natural numbers to ensure well-typedness, which is not only tedious but some of it also ends up happening at run-time. Since type-level natural numbers are represented in unary, this could be a source of inefficiency in the future. However, it has so far proven very effective at avoiding bugs!

Another interesting tool used in the implementation is a technique for writing generic traversal functions for data structures. With heterogeneous type-indexed lists, we can write a single traversal function that can be called with arbitrarily many data structures as input and arbitrarily many as output, thus including in particular map, map2, iter (the 0-output case), iter2, and so on. If this generic traversal is parametrized over a monad, or more generally an applicative functor, then it also includes both left and right folds, possibly combined with maps, and so on. For a simple data structure like lists this is overkill, of course, but for some of the complicated data structures we use (like n-dimensional cubes that are statically guaranteed to have exactly the right number of elements, accessed by giving a face) it saves a lot of work to be able to implement only one traversal.

The source code is organized in directories as follows:

  • lib/: Most of the code

    • lib/util/: Utilities that could in principle be generic libraries

    • lib/dim/: Definition of the dimension theory (cube category)

    • lib/core/: Syntax, normalization, type-checking, etc.

    • lib/parser/: Parsing and printing

    • lib/top/: Auxiliary functions for the top-level (executing files, etc.)

  • bin/: The main executable

  • test/: Unit tests