When should I use De Bruijn levels instead of indices?

Question

I am familiar with De Bruijn indices, but not with De Bruijn levels. In my understanding, indices index variables from the top of the context/stack, whereas levels index variables from the bottom. So indices might be more attractive for dealing with bindings, but levels might be more attractive for dealing with weakening. But how does this play out from a broader perspective, for example when building an evaluator or a typechecker?

In what instances should De Bruijn levels be used over De Bruijn indices, and vice versa?

Answer 1

If we want to do evaluation in the presence of free variables ("open" evaluation), then De Bruijn levels are essential, precisely because of their support for cost-free weakening.

Generally, the best practice to implement substitutions and beta-reductions with open terms, is to have

1. Syntactic terms, which can be evaluated to values in a given value environment. These may use any variable representation, but usually De Bruijn indices are the simplest and most efficient.
2. Values, which contain closures instead of binders. Values must use levels or some other variable representation which is not relative to the size of the scope (e.g. globally fresh names are also workable).

The combination of levels and closures is what allows free weakening of values. If we have levels in plain terms, the bound variables have to be shifted during weakening. But here we don't have bound variables, we have closures instead, so there is nothing to shift.

For open evaluation of pure lambda terms, it looks like the following (in Haskell):

type Ix  = Int
type Lvl = Int

data Tm      = Var Ix | Lam Tm | App Tm Tm
data Closure = Close [Val] Tm
data Val     = VVar Lvl | VApp Val Val | VLam Closure

eval :: [Val] -> Tm -> Val
eval env t = case t of
  Var x   -> env !! x
  App t u -> case (eval env t, eval env u) of
               (VLam (Close env' t), u) -> eval (u:env') t
               (t                  , u) -> VApp t u
  Lam t   -> VLam (Close env t)

We may also add quoting to normal forms, to get normalization-by-evaluation:

quote :: Lvl -> Val -> Tm
quote l t = case t of
  VVar x             -> Var (l - x - 1)
  VApp t u           -> App (quote l t) (quote l u)
  VLam (Close env t) -> Lam (quote (l + 1) (eval (VVar l:env) t))

nf :: [Val] -> Tm -> Tm
nf env t = quote (length env) (eval env t)

Some sources which use this basic evaluation setup:

• Thierry Coquand: An algorithm for type-checking dependent types
• Abel, Coquand, Pagano: A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Coquand et al.: A simple type-theoretic language: Mini-TT
• David Christiansen: Checking Dependent Types with Normalization by Evaluation: A Tutorial
• cubicaltt
• cooltt
• My elaboration zoo