(WIP) Dependent language series, part 0

2025-05-08

Assumed knowledge

You should at least be familiar with dependent types, using a language such as Agda, Rocq, Idris, or Lean. This series will primarily use Agda syntax.

Supplimentary

I highly recommend András Kovács' "Elaboration Zoo", found at this link, as something akin to a source of truth. If this blog series and the Elaboration Zoo explicitly contradict, assume that it is correct (and please contact me!).

Motivation (Why learn this, anyway?)

TODO (slightly ironic, I know)

De Bruijn and why we use it

Let's look at a little imaginary term, in some language.

λ f. (λ y f. (f y)) f

We can perform what's called "beta reduction" on this term — essentially, applying f to the lambda.

λ f. (λ y f. (f y)) (f)

substitute [y := f] in λ y f. (f y)

λ f. (λ f. f f)

Uh oh. We've accidentally captured a variable! Instead of f referring to the outer f, now it refers to the inner f. This is "the capture problem", and it is quite annoying. Generally to avoid this, we need to rename everything in our "substituted" term to names that are free (do not occur) in the "subsitutee" so nothing is accidentally captured. What if we could introduce a notation that completely avoids this?

Presenting: De Bruijn Indexes!

De Bruijn indexes are a naming scheme where:

We use natural numbers to refer to lambdas, and
Zero refers to the "most recent" lambda; one refers to the second most recent, etc.

Let's rewrite that term above using this system:

λ (λ λ (0 1)) 0

Here's some ascii art showing what refers to what:

 λ   (λ   λ   (0   1))   0
 |    |    \———/   |     |
 |    |            |     |
 |    \————————————/     |
 \———————————————————————/

Now, how does this help us with our substituion problem? Surely if we naively subtitute we will still have binding issues - and indeed we do:

λ (λ λ (0 1)) 0
->
λ (λ (0 0))

No good!

What De Bruijn indexes allow us to do is simply avoid capturing. The rule is simple: Every time we go past a binder when substituting, we increment every free variable¹ in our substituted by one, to avoid the new binder:

 λ (λ λ (0 1)) 0
 ->
 λ (λ (0 1))
 ^  ^    ^ incremented by one when we passed "through" lambda b
 |  |
 |  \ lambda b
 |
 \ lambda a

Now we're cool! Everything works as expected, and it takes much less work (and is much more predictable!).

Presenting: De Bruijn levels!

De Bruijn levels work similar to De Bruijn indexes, in that we use numbers to refer to binders. However, in De Bruijn levels, the lowest number refers to the least recently bound item.

Recall that:

Named:   λ f. (λ y f. (f y)) f
Indexes: λ (λ λ (0 1)) 0

Now, with levels:

Levels:  λ (λ λ (2 1)) 0

This has the same diagram of what refers to what:

 λ   (λ   λ   (2   1))   0
 |    |    \———/   |     |
 |    |            |     |
 |    \————————————/     |
 \———————————————————————/

(As it should! These two representations represent the same term.)

As you might expect, de Bruijn indexes and levels are each beneficial in their own situations.

Generally, De Bruijn indexes are "more useful" than De Bruijn levels, as they're "more local". In order to work with levels, you need to know "how deep" you are in a term at all times.

De Bruijn indexes give us the advantage that we can freely create new binders without the need for any information about where in a term we are, whereas de Bruijn levels give us the advantage when moving a term under a binder, free variables do not need to be modified.

 λ (λ λ (2 1)) 0
               ^ this zero...
 ->
 λ (λ (1 0))
       ^ ^ is still zero!
       |
       \ we had to modify this one though

De Bruijn Wrapup

De Bruijn indexes and levels can also be summed up via the following:

λa. λb. λc. c

indexes:
λ λ λ 0
^ ^ ^
2 1 0

levels:
λ λ λ 2
^ ^ ^
0 1 2

if you’re “here”

  v
λ λ λ

Using indexes, adding anything binders further left doesn’t affect the current binder's variables, or any further right.
Using levels, adding anything binders further right doesn’t affect the current binder's variables, or any further left.

Evaluation while typechecking

Complex dependent types require computation while typechecking. Consider the following:

neg-or-not : (b : Bool) -> if b then (Int -> Int) else (Bool -> Bool)
neg-or-not true x = -x
neg-or-not false x = not x

When we wish to typecheck neg-or-not true x, we must evaluate in the type of neg-or-not in order to be able to tell what the type of x should be. This means our typechecker is going to have evaluation in it! Unlike with "normal" runtime evaluation, this evaluation is compile time, and hence we wish to control it as much as possible. We do not want to be fully computing every term, as that's slow and unnecessary. There are several evaluation techniques that achieve various levels of this — the one we will be exploring is called "Normalization by Evaluation" (NbE). As the title alludes to, the goal of NbE is to normalize a term to our desired "weak normal form"² using evaluation, and then stop evaluating at that normal form. Evaluating to this weak normal form guarantees two things:

We do not do excess work. If a value in a let is not used, for example, we will never fully evaluate it. This will be elaborated on in part 1 (coming soon™️), but it is a deliberate consequence of choosing a weak normal form.
That two elements can be immediately compared for shallow equality without "excess" work. We will often need to compare terms fully, which will imply fully evaluating them, but it is worth remembering that programmers often write incorrect programs, so bailing early can be beneficial to performance.

The core ideas of NbE are as follows:

Have two representations of your program: A "term language" and a "value language".
The term language represents any given term, with no restrictions (except being type correct).
The value language represents only terms in a normal form², correct-by-construction. (It is only possible to form elements of the value type if they are in a normal form.)
The term language uses De Bruijn indexes, as they are more suitable for direct translation from user input, and do not rely on knowing "nonlocal information" in order to create new binders.
The value language uses De Bruijn levels, so that values can be placed under binders without the need for modification.
We have a function, called "evalutate" or "eval", that takes expressions in the term language to the value language (i.e., reduces them to normal form through evaluation).
We have a function, called "quote", that takes expressions in the value language back to the term language.

Using NbE as a basis, we can then build a typechecker for a dependent language! We will have the tools in place to be able to properly reduce dependent types, allowing for typechecking of non-reduced values.

Notes for the next part

This series will primarily be in OCaml. I am aiming to stick to simple features ---