1001 Representations of Syntax with Binding

Posted by Jesper on November 4, 2021

As a compiler developer or programming language researcher, one very common question is how to represent the syntax of a programming language in order to interpret, compile, analyze, optimize, and/or transform it.

One of the first lessons you learn is to not represent syntax as the literal string of characters written by the programmer, but rather convert it to an abstract syntax tree (AST). This has a number of advantages: it enforces structure on programs, makes the syntax easier to traverse and transform, erases irrelevant details (e.g. whitespace and comments), and allows for better separation of different intermediate states of the syntax.

However, syntax is in fact not a tree but a graph: names (of variables, functions, classes, modules, …) can point to potentially far-away locations in the program’s text. The way these work is that one occurrence of the name binds the name (aka the binder), and other occurrences of the same name mention the name, thus pointing to the binder.

Just as representing syntax as a string is not a good idea for most purposes, representing names as strings is usually not a good idea either. This will be clear to anyone who has ever implemented capture-avoiding substitution for lambda-terms with strings as variable names (and if you haven’t, I invite you to do so). Hence we would like to have a generic and universal way to represent the structure of binders-and-mentions, similar to how abstract syntax trees represent the structure of syntactical-constructs-and-their-components.

Unfortunately, in contrast to the case of abstract syntax, there are countless different techniques, frameworks, and meta-languages for dealing with name binding, none of which come close to be universally accepted or clearly superior to the others. For the compiler developer or PL researcher who just wants to define their syntax and move on to more interesting things, this is frustrating, to say the least. Make the wrong choice, and you are stuck with impossibly complex and buggy code for manipulating variables, or proving an endless stream of substitution lemmas, or figuring out too late that the thing you want to do is just not possible with the chosen representation of names.

In this post, I will give an overview of all the different techniques for implementing syntax with binders in Agda that I could find. With each technique, I will show how to use it in Agda to represent the syntax of (untyped) lambda calculus, and also explain briefly what the main motivation is for using it. I hope this will be useful to you for making an informed choice between these options.

Since there’s quite a few of them, I can only give a brief description of each representation in this post. If you want to learn more about any of them, you can find my full list of references on Researchr. Also, since this is a blog post and not a book, I will limit this overview to representations that can be defined and used in Agda or a similar dependently-typed functional language (e.g. Coq or Haskell), not in language features that could be added to Agda or in entire new languages built for this specific purpose. In particular, this means representations that require a (meta-)language with a built-in way to assign unique identifiers are ruled out.

Finally, in this post I will not consider the problem of name resolution, i.e. how to figure out which binder each occurrence of a name points to. Instead, I focus on how to represent and manipulate syntax where names are used correctly according to the rules of the language. You can think of this as finding a good representation of the output of name resolution, similar to how an AST is the output of parsing.

With these disclaimers in place, it is time to start with the first and possibly most ubiqitous representation: de Bruijn indices.

De Bruijn indices

De Bruijn indices are the most common nameless representation of name binding. A de Bruijn index represents a name by counting how many binders need to be skipped when traversing upwards through the AST before one reaches the name’s binding site.

Here is the definition of lambda terms using de Bruijn indices, and a representation of the term λ f. λ x. f x:

module DeBruijnSyntax where
  data Term : Set where
    var :   Term
    lam : Term  Term
    app : Term  Term  Term

  ex : Term
  ex = lam {-f-} (lam {-x-} (app (var {-f-} 1) (var {-x-} 0)))

De Bruijn syntax is used widely in the implementation and formalization of programming languages, especially with functional implementation languages. For example, Agda is implemented in Haskell and the internal syntax represents variables (but not other names) using de Bruijn indices.

The big advantage of de Bruijn syntax is that each lambda-expression has a unique representation and hence any two α-equivalent terms (e.g. λ x. x and λ y. y) are represented the same. It also leads to a more uniform and - arguably - more pleasant implementation of substitution than on syntax with strings for names. On the other hand, it is often quoted as a good “reverse Turing test” because most humans have a hard time grasping the meaning of a term and reasoning about them correctly.

A variation on de Bruijn indices are de Bruijn levels, which count the number of binders starting from the root node rather than from the occurrence of the name. This simplifies the implementation of some operations, but the assumption there exists a global ‘root node’ complicates others, so overall the choice between de Bruijn indices and levels is kind of a wash.

Locally nameless

One of the main problems with de Bruijn syntax is the absence of any actual names when constructing syntax. One possible solution is to distinguish between variables that are bound and those that are free, and note that only bound variables need to be anonymous. This leads to the class of syntax representations known as locally nameless.

module LocallyNameless where

  Name = String

  data Term : Set where
    bound :   Term
    free  : Name  Term
    lam   : Term  Term
    app   : Term  Term  Term

To mediate between bound and free variables (e.g. when going under a binder), we define operations for opening and closing a term:

  openUnder :   Name  Term  Term
  openUnder k x (bound n) =
    if does (k ℕ.≟ n) then free x else bound n
  openUnder k x (free y)  = free y
  openUnder k x (lam u)   = lam (openUnder (suc k) x u)
  openUnder k x (app u v) =
    app (openUnder k x u) (openUnder k x v)

  openT = openUnder 0

  closeUnder :   Name  Term  Term
  closeUnder k x (bound n) = bound n
  closeUnder k x (free y)  =
    if does (x String.≟ y) then bound k else free y
  closeUnder k x (lam u)   = lam (closeUnder (suc k) x u)
  closeUnder k x (app u v) =
    app (closeUnder k x u) (closeUnder k x v)

  closeT = closeUnder 0

Using closeT, we can write down variables as strings but convert them to de Bruijn indices on the fly:

  ex = lam (closeT "f" (
         lam (closeT "x" (
           app (free "f") (free "x")

  _ : ex  lam (lam (app (bound 1) (bound 0)))
  _ = refl

There are many possible variants of the locally nameless style, where either the representation of either free or bound variables differs. For example, representing both free and bound variables as names (from two distinct types) leads to the locally named representation, which was actually introduced first. In the other direction, instead of representing free variables as strings one could instead represent them as de Bruijn levels, which results in an interesting combination of de Bruijn indices and de Bruijn levels.

Locally nameless syntax representations have been successfully used for doing formal metatheory in Coq, including the formalization of PCUIC for the MetaCoq project. However, using it successfully requires a lot of boilerplate for dealing with opening and closing of terms, which might be prohibiting unless the boilerplate can be generated automatically. Repeated opening and closing of terms might also introduce a performance bottleneck when this approach is used for a practical implementation and not just doing metatheory.

Nominal signatures

Next to the broad family of nameless representations based on de Bruijn’s representation, a wholly different way to think about names is by relying on nominal techniques. Very briefly speaking, this means we rely on the presence of one or more abstract sorts of atoms (i.e. names) together with an operation for swapping two atoms in a term and a predicate expressing freshness of an atom with respect to a term. On top of these, one can define a sort constructor for abstracting over a single atom/name (I am deliberately using the word ‘sort’ instead of ‘type’ since these are not regular Agda types). We can then use name abstraction directly to write down a signature of our syntax and its induction principle.

While nominal techniques provide a general approach to define and reason about syntax with binders, I actually hesitate to include it here because it seems to require special language support to use effectively, which Agda does not have. However, we can work around that problem by defining a record type that specifies an abstract interface for working with atoms and (nominal) sorts (here I simplify it to a single sort of atoms):

module Nominal where
  record Nominal : Set₂ where
      Sort  : Set₁
      Atom  : Sort
      1ᵉ    : Sort
      _×ᵉ_  : Sort  Sort  Sort
      _→ᵉ_  : Sort  Sort  Set
      absᵉ  : Sort  Sort
      -- lots of axioms omitted
  open Nominal {{...}}

The interface first declares a type Sort of sorts, and a particular sort Atom of atoms. It also contains fields for the analogues of regular Agda type constructors on sorts, such as pairs, functions, and predicates. We then declare that for each sort A, we have another sort absᵉ A of elements of A abstracted over a single (unknown) name. Finally, although I didn’t write them here, if you would actually want to use this you would also need lots of other fields with axioms to specify freshness, as well as how to instantiate an element of absᵉ A with a fresh variable.

Once we have declared this abstract interface, we can use it to declare our syntax. Since Agda does not allow defining datatypes in an abstract type such as Sort, we once again resort to an abstract interface for declaring the syntax.

  module _ {{_ : Nominal}} where
    record Syntax : Set₁ where
        Term : Sort
        var  : Atom →ᵉ Term
        app  : (Term ×ᵉ Term) →ᵉ Term
        lam  : (absᵉ Term) →ᵉ Term
        -- induction principle omitted

Since these interfaces are abstract, an important question is whether it is actually possible to implement them - otherwise they’d be pretty useless. The traditional way to do this relies on the presence of nominal sets - sets with built-in operations for swapping and freshness - for which I am not sure how easy they are to define in Agda. Luckily, we don’t have to, as there is an easier way to implement the Nominal and Syntax interfaces in terms of the “Namely, Painless” approach by Nicolas Pouillard (see the section on it further down below).

Higher-order abstract syntax

Instead of trying to find a good encoding of variables for our syntax, it is tempting to instead try to re-use the existing variable binding capabilities of our meta-language (Agda). This third approach (after nameless and nominal techniques) is known as higher-order abstract syntax. A naive attempt at using this in Agda goes as follows:

module ‶HOAS″ where
  data Term : Set where
    lam : (Term  Term)  Term
    app : Term  Term  Term

  ex : Term
  ex = lam  f  lam  x  app f x))

There is no explicit case for variables in the syntax, instead variables are meta-level variables of type Term. The scoping discipline of the meta-language thus enforces that variables cannot be used outside of their scope, i.e. terms are well-scoped by construction. In addition, we get the nice property of de Bruijn syntax that any two α-equivalent terms are equal. Moreover, substitution can be implemented simply by function application on the meta-level.

But (and this is a very big but) this approach does not actually work. First of all, this type of terms is not strictly positive (as indicated by the big NO_POSITIVITY_CHECK pragma on top) and can in fact easily be exploited to define a non-normalizing term, thus breaking Agda’s termination guarantees. Another huge problem is that it is not possible to match on a term to see if it is a variable, so many algorithms on the syntax (such as checking syntactic equality) are simply impossible to implement. In addition, this representation allows defining so-called ‘exotic terms’ that pattern match on the syntactic structure of a variable, which should not be possible in the syntax of our language:

  exotic : Term
  exotic = lam  x  case x of λ where
                        (lam _)    x
                        (app _ _)  lam  y  y))

Because of all these problems, most people would not consider this type to be ‘real’ HOAS, and instead reserve the term for languages that actually support a weak function space, such as Twelf, Beluga, or Dedukti.

A variant of HOAS that can be used effectively in a language without a weak function space is parametric higher-order abstract syntax (PHOAS). Instead of representing variables directly as meta-level variables of type Term, they are instead encoded as elements of an abstract type V, and there is an explicit constructor var for variables:

module PHOAS where
  data Term (V : Set) : Set where
    var : V  Term V
    lam : (V  Term V)  Term V
    app : Term V  Term V  Term V

  ex :  {V}  Term V
  ex = lam  f  lam  x  app (var f) (var x)))

This type does not suffer from issues with positivity, it is possible to check whether a term is a variable, and exotic terms are ruled out since there is no way to pattern match on an element of the abstract type parameter V. Yet it preserves the good property that terms are well-scoped by construction and that α-equivalent terms are equal.

Still, just from the fact that it is a higher-order representation, PHOAS can be challenging to use in practice. In particular, defining simple operations involves coming up with clever ways to instantiate the parameter V; for example pretty-printing a term can be done by instantiating V to be String:

  pp :   Term String  String
  pp fresh (var x)    = x
  pp fresh (lam f)    =
    let name = "x" ++ ℕ.show fresh
    in  "λ " ++ name ++ ". " ++ pp (suc fresh) (f name)
  pp fresh (app u v)  = case u of λ where
    (var x)  x ++ " " ++ pp fresh v
    _        "(" ++ pp fresh u ++ ") " ++ pp fresh v

  _ : pp 0 ex  "λ x0. λ x1. x0 x1"
  _ = refl

Other algorithms might require functional extensionality or parametricity results to reason correctly about the behaviour of the syntax. Altogether, it seems to me these reasons imply PHOAS is less well suited for implementing actual algorithms on syntax, as opposed to purely doing metatheory (for which it was originally introduced).

Well-scoped de Bruijn indices

If all we want from PHOAS is the fact that terms are well-scoped by construction, there is actually a much easier way to obtain that guarantee with de Bruijn indices: we can simply index the type by the number n of variables that are in scope, and require that indices are elements of Fin n. This is known as well-scoped de Bruijn syntax.

module WellScopedDB where
  data Term (n : ) : Set where
    var : Fin n  Term n
    lam : Term (1 + n)  Term n
    app : Term n  Term n  Term n

  ex : Term 0
  ex = lam {-f-} (
         lam {-x-} (
           app (var {-f-} (suc zero))
               (var {-x-} zero)

One could criticize this for relying on dependent types in the meta-language. However, we can obtain a variant of well-typed de Bruijn syntax that does not require the use of dependent types by indexing directly by the set of variables in scope:

module PoorMansWellScoped where
  data Term (V : Set) : Set where
    var : V  Term V
    lam : Term (Maybe V)  Term V
    app : Term V  Term V  Term V

  ex : Term 
  ex = lam {-f-} (
         lam {-x-} (
           app (var {-f-} (just nothing))
               (var {-x-} nothing)

This provides the same guarantees as well-scoped de Bruijn syntax, but can be implemented in Haskell ’98. However, elements of nested Maybe types are a bit harder to manipulate than elements of type Fin, and may lead to worse performance if Fins end up being represented as machine integers. Also, you should just use a proper language that supports dependent types instead.

A more serious criticism I have against this representation is that while this representation makes it harder to write wrong transformations on syntax that mess up the variables, it does not really do anything to make good de Bruijn terms easier to produce or understand for humans. For example, a term of type Term 2 with two variables x and y in scope does not indicate whether x is var 0 and y is var 1 or vice versa.

Still, well-scoped de Bruijn syntax is used quite often in practice, for example in the generic-syntax library for Agda. In fact, this library goes beyond the subject of this blog post in many ways, by providing a generic universe of syntaxes with generic operations defined over them and by enforcing not just well-scopedness but also well-typedness. While these features are orthogonal to the topic of this blog post, I strongly encourage you to take a look at it.

Well-scoped names

One criticism we had of de Bruijn syntax is the fact that it is very hard to understand by humans, and this problem is not really solved by switching to the well-scoped variant. We can solve this problem by - instead of indexing by just the number of variables in scope - indexing by the scope itself, represented as a list of names. Variables then contain two pieces of data: a name and a proof that the name is in scope.

module WellScopedNames where
  open import Data.List.Membership.Propositional using (_∈_)
  open import Data.List.Relation.Unary.Any using (here; there)

  Scope = List String

  data Term (s : Scope) : Set where
    var : (x : String)  x  s  Term s
    lam : (x : String)  Term (x  s)  Term s
    app : Term s  Term s  Term s

  ex : Term []
  ex = lam "f" (
         lam "x" (
           app (var "f" (there (here refl)))
               (var "x" (here refl))

The result we get is a combination of named variables with well-scoped de Bruijn syntax. While the membership proofs are cumbersome to write by hand, it wouldn’t take much effort to implement a macro that constructs them automatically.

While there is no fundamental difference in the guarantees offered by this representation and well-scoped de Bruijn syntax, having the names around is more intuitive for the programmer and can help to avoid errors when changing the order of variables in scope. However, having the names around also means we lose one advantage of de Bruijn syntax: two α-equivalent terms can now be distinguished by looking at the names of the variables.

One other thing one should keep in mind when using this representation is that it allows referring to shadowed names. For example, it is perfectly fine to name both variables x in the previous example:

  ex' : Term []
  ex' = lam "x" (
          lam "x" (
            app (var "x" (there (here refl)))
                (var "x" (here refl))

The reason for this is that the membership proof x ∈ s is proof-relevant: it consists of a path to the position where the variable is bound in the scope. While this can be considered as either a feature or a bug, it does mean one has to be careful with pretty-printing, since a naive approach would print the above term as λ x. λ x. x x, which is not correct. If desired, we could instead use a more sophisticated representations of scopes that enforces freshness as an inductive-recursive type:

module WellScopedFresh where

  data FreshList (A : Set) : Set
  _#_ : {A : Set}  A  FreshList A  Set

  data FreshList A where
    []    : FreshList A
    _∷_<_> : (x : A) (xs : FreshList A)  x # xs  FreshList A

  x # [] = 
  x # (y  xs < _ >) = x  y × (x # xs)

  data _∈_ {A : Set} (x : A) : FreshList A  Set where
    here  :  {xs p}  x  (x  xs < p >)
    there :  {y xs p}  x  xs  x  (y  xs < p >)

  Scope = FreshList String

  data Term (s : Scope) : Set where
    var : (x : String)  x  s  Term s
    lam : (x : String) (p : x # s)
         Term (x  s < p >)  Term s
    app : Term s  Term s  Term s

  ex : Term []
  ex = lam "f" f# (
         lam "x" x#f (
           app (var "f" (there here))
               (var "x" here)
      f# : "f" # []
      f# = tt

      x#f : "x" # ("f"  [] < f# >)
      x#f =  ()) , tt

As you can see, this approach ensures that the names we bind are fresh w.r.t. the current scope, at the cost of more complex types and having to produce freshness proofs (although this could also be automated).

Despite its limitations I feel that the simple version using a normal list of names strikes a nice balance between getting good static guarantees and being easy to use. This is also attested by the fact it is used in the bootstrapped implementation of Idris 2.

Nameless, Painless

When I explained the nominal approach to name binding, I made use of an abstract interface exposing the operations. While this was done out of necessity (since Agda does not have nominal types built-in), working with an abstract interface for name binding actually has other benefits: it allows us to avoid relying on the implementation details of names by hiding them from the interface, and it even allows swapping out a concrete implementation of variables for another one (perhaps one that’s more efficient).

This is what the paper “Nameless, Painless” does: it provides an abstract interface to well-scoped de Bruijn indices. The interface consists of an abstract type of Worlds (i.e. scopes), and for each world w a set of names Name w. In the concrete implementation of well-scoped de Bruijn syntax we gave above, these were implemented as World = ℕ and Name = Fin respectively.

module NamelessPainless where

  record NaPa : Set₁ where
      World   : Set
             : World
      _↑1     : World  World
      Name    : World  Set
      _⊆_     : World  World  Set
      zeroᴺ   :  {α}  Name (α ↑1)
      sucᴺ    :  {α}  Name α  Name (α ↑1)
      _==ᴺ_   :  {α}  Name α  Name α  Bool
      exportᴺ :  {α}  Name (α ↑1)  Maybe (Name α)
      coerce  :  {α β}  α  β  Name α  Name β
      ¬Name∅  : ¬ (Name )

  open NaPa {{...}}

The operation _==ᴺ_ allows us to compare two names in the same scope, and the function exportᴺ allows us to do case analysis on whether a name is bound by the top-level binder or one beneath it.

To actually define a syntax that uses this interface, we parametrize our module with an instance argument of type NaPa:

  module _ {{_ : NaPa}} where

    data Term (w : World) : Set where
      var : Name w  Term w
      lam : Term (w ↑1)  Term w
      app : Term w  Term w  Term w

    ex :  {w}  Term w
    ex = lam {-f-} (
           lam {-x-} (
             app (var {-f-} (sucᴺ zeroᴺ))
                 (var {-x-} zeroᴺ)

Apart from the benefits mentioned above, we also get additional free theorems as a result of being parametric over the implementation of scopes and names. For example, the paper shows that any world-polymorphic function commutes with renaming of the free variables.

Despite these apparent strengths, I have not seen this approach being used in practice. I’m not sure that’s because it has some important downsides, or just because it is not well known.

Abstract scope graphs

Scope graphs provide a very general interface for representing syntax with name binding and name resolution. Broadly speaking, nodes in a scope graph represent scopes, and edges determine reachability. Rather than formalize the full theory of scope graphs here, we can take the same approach as before and declare an abstract interface containing the pieces we need here (I apologize to my colleagues in Delft if I am horribly misrepresenting scope graphs):

module AbstractScopeGraphs where

  Name = String -- just for concreteness

  record ScopeGraph : Set₁ where
      -- Structure of scope graphs we rely on:
      -- 1. a type of scopes (i.e. nodes in the graph)
      Scope : Set
      -- 2. a predicate expressing reachability + visibility
      _∈_   : Name  Scope  Set
      -- 3. Binding a name, shadowing all previous occurrences
      bind  : Name  Scope  Scope
      here  :  {x s}  x  bind x s
      there :  {x y s}  x  y  x  s  x  bind y s

  open ScopeGraph {{...}}

The definition of a scope graph relies on two core notions of reachability and visibility of a name in a scope. For simplicity both of them are combined into a single predicate _∈_ in this interface. We can then define our syntax using _∈_ and bind:

  module _ {{_ : ScopeGraph}} where

    data Term (s : Scope) : Set where
      var : (x : Name)  x  s  Term s
      lam : (x : Name)  Term (bind x s)  Term s
      app : Term s  Term s  Term s

    ex :  {s}  Term s
    ex {s} = lam "f" (
               lam "x" (
                 app (var "f" (there  ()) here))
                     (var "x" here)

The result is very similar to the approach using FreshList we defined above, except that now we use an abstract interface as in the Nameless, Painless approach. This means it is easier to extend the interface with more fine-grained notions (e.g. the distinction between reachability and visibility) that scope graphs allow us to model. It also allows us to scale up more easily to more complex name binding structures.

There’s still an issue that this approach shares with the FreshList approach: since the syntax of a lambda expression contains an element of type Name, it is possible to distinguish two α-equivalent names. Another possible drawback is that much of the generality of scope graphs is not actually needed, which might result in unneeded complexity (though the use of an abstract interface means this does not matter too much).

The ‘Namely, Painless’ approach

In his PhD thesis, Nicolas Pouillard (the main author of the “Nameless, Painless” paper) presents another interface for programming with names and binders called NomPa (for “Nominal, Painless”, I presume). In contrast to NaPa, it models syntax with named variables. Yet it avoids the problem discussed above, so α-equivalent terms are indistinguishable. The trick here is to have separate types for names and binders, and only expose equality checking of names in the interface:

module NamelyPainless where

  record NomPa : Set₁ where

      World  : Set
      Name   : World  Set
      Binder : Set
      _◃_    : Binder  World  World

      zeroᴮ  : Binder
      sucᴮ   : Binder  Binder

      nameᴮ   :  {α} b  Name (b  α)
      binderᴺ :  {α}  Name α  Binder

            : World
      ¬Name∅ : ¬ (Name )

      _==ᴺ_   :  {α} (x y : Name α)  Bool
      exportᴺ :  {α b}  Name (b  α)
               Name (b  )  Name α

      _#_  : Binder  World  Set
      _#∅  :  b  b # 
      suc# :  {α b}  b # α  (sucᴮ b) # (b  α)

      _⊆_     : World  World  Set
      coerceᴺ :  {α b}  α  b  Name α  Name b
      ⊆-refl  : Reflexive _⊆_
      ⊆-trans : Transitive _⊆_
      ⊆-∅     :  {α}    α
      ⊆-◃     :  {α β} b  α  β  (b  α)  (b  β)
      ⊆-#     :  {α b}  b # α  α  (b  α)

  open NomPa {{...}}

Note that names are bound to a specific world, so there is no way to compare names from different worlds.

  module Syntax {{_ : NomPa}} where

    data Term (w : World) : Set where
      var : Name w  Term w
      lam : (b : Binder)  Term (b  w)  Term w
      app : Term w  Term w  Term w

    ex : Term 
    ex = lam fb (lam xb (app (var f) (var x)))
        fb xb : Binder
        fb = zeroᴮ
        xb = sucᴮ zeroᴮ

        x-fresh : xb # (fb  )
        x-fresh = suc# (fb #∅)

        f = coerceᴺ (⊆-# x-fresh) (nameᴮ fb)
        x = nameᴮ xb

Just as with NaPa, we get nice free theorems by being parametric in the implementation of NomPa. For example, the parametricity theorem for _==ᴺ_ tells us that checking equality commutes with renaming, hence α-equivalent terms are indeed treated equally.

As promised earlier, NomPa can be used to implement the interface we previously used for nominal signatures:

  module NominalNomPa {{_ : NomPa}} where
    Sort : Set₁
    Sort = World  Set

    Atom : Sort
    Atom = Name

    1ᵉ : Sort
    1ᵉ _ = 

    _×ᵉ_ : Sort  Sort  Sort
    (E₁ ×ᵉ E₂) a = E₁ a × E₂ a

    _→ᵉ_ : Sort  Sort  Set
    (E₁ →ᵉ E₂) =  {a}  E₁ a  E₂ a

    Pred   : Sort  Set₁
    Pred E =  {a}  E a  Set

    absᵉ : Sort  Sort
    (absᵉ E) a = Σ[ b  Binder ] (E (b  a))

    data Term : Sort where
      var : Atom →ᵉ Term
      app : (Term ×ᵉ Term) →ᵉ Term
      lam : (absᵉ Term) →ᵉ Term

To check that this indeed results in a valid implementation of the nominal interfaces we wrote down before, we can instantiate the interfaces elegantly using the little-known syntax for building record values from modules.

    nominal : {{_ : NomPa}}  Nominal.Nominal
    nominal = record { NominalNomPa }

    nominalSyntax : {{_ : NomPa}}  Nominal.Syntax
    nominalSyntax = record { NominalNomPa }

NomPa has all the desirable properties of the various approaches mentioned before, and can in fact be used to model these approaches. So, is it the ultimate approach to modelling name binding in Agda? Well, who knows, as once again I have not found anywhere it is actually used, despite it being published in 2012. My main worry is that the interface is quite large, and hence could be complicated to use in practice.

Co-de Bruijn indices

Since the invention of NomPa, there has been at least one more exciting development in the area of syntax with binders. In his 2018 paper “Everybody’s Got To Be Somewhere”, Conor McBride describes co-deBruijn syntax, a nameless representation where binding information is encoded completely in the structure of the terms rather than at the variables themselves. In particular, each term constructor remembers which variables are actually used by which subterm, removing the rest from the scope. When we arrive at a variable, all the unused variables have been removed from the scope, so there is but a single variable to pick.

Brutally stripping all the categorical concepts from the paper, one might end up with the following simplified type of scope coverings:

module CoDeBruijn where

    k l m n : 

  data Cover : (k l m : )  Set where
    done   :               Cover      0       0       0
    left   : Cover k l m  Cover (suc k)      l  (suc m)
    right  : Cover k l m  Cover      k  (suc l) (suc m)
    both   : Cover k l m  Cover (suc k) (suc l) (suc m)

An element of type Cover k l m says for each of m variables whether they are used just in the left subterm, just in the right subterm, or in both subterms. The left and right subterms thus should have k and l variables in scope respectively. Crucially there is no case for neither, hence the slogan “everybody’s got to be somewhere”.

We can then define our well-scoped co-deBruijn syntax using Cover:

  data Term :   Set where
    var  : Term 1
    lam  : Term (suc n)  Term n
    lam' : Term n  Term n  -- argument is not used
    app  : Cover k l m  Term k  Term l  Term m

  ex : Term 0
  ex = lam {-f-} (
         lam {-x-} (
           app (right (left done))
               (var {-f-}) (var {-x-})

There are two constructors for lambda abstraction: one for functions that use their argument and one for functions that don’t (I’m sure there’s a more elegant way to do this, but this works).

The great advantage of using co-deBruijn syntax is that scopes are always maximally precise: there is never any need to strengthen a term to get rid of an unused variable. On the flip side, co-deBruijn syntax is even more unintuitive and difficult to understand for humans than regular de Bruijn syntax. Quoting the author: “Co-de-Bruijn representation is even less suited to human comprehension than de Bruijn syntax, but its informative precision makes it all the more useful for machines. Dependency checking is direct, so syntactic forms like vacuous functions or η-redexes are easy to spot.”

To make the syntax more comprehensible to mere mortals, we can do the same we did for de Bruijn syntax and represent scopes as lists of names:

module NamedCoDeBruijn where

  Name  = String
  Scope = List Name

    x y z    : Name
    xs ys zs : Scope

  data Cover : (xs ys zs : Scope)  Set where
    done   :                  Cover      []       []       []
    left   : Cover xs ys zs  Cover (z  xs)      ys  (z  zs)
    right  : Cover xs ys zs  Cover      xs  (z  ys) (z  zs)
    both   : Cover xs ys zs  Cover (z  xs) (z  ys) (z  zs)

Doing this leads to a syntax that is much more pleasant to use (at least if we pick unique names):

  data Term : Scope  Set where
    var  : (x : Name)  Term (x  [])
    lam  : (x : Name)  Term (x  xs)  Term xs
    lam' : (x : Name)  Term xs  Term xs
    app  : Cover xs ys zs  Term xs  Term ys  Term zs

  ex : Term []
  ex = lam "f" (
         lam "x" (
           app (right (left done))
               (var "f") (var "x")

The remaining ugliness is the Cover proof needed at each application, however as before writing a macro that constructs these automatically should not be difficult.

One could imagine generalizing this further and defining an abstract interface like NomPa for working with co-deBruijn syntax. However, this post is plenty long as it is, so I’ll leave that as an exercise to the reader.

Overview and conclusion

The goal of this blog post was mainly to give an overview of the various different approaches one could use when defining syntax with binders in Agda. Below is a table summarizing with the approaches I described, plus the benefits they provide to the programmer:

So here’s the full table:

First-order representation X X X X X X X X X X X X
Named variables X X X X X X X X X
Enforces α-equivalence X X X X X X X
Enforces well-scopedness X X X X X X X X X
No mixing of scopes X X X X X
Enforces freshness X X X X
Abstract interface X X X X
Strengthening is no-op X X X

As a next step, it would be interesting to perform a comparison of (some of) these approaches on a practical application. My idea would be to define variants of the reflection syntax of Agda using a few different approaches (it currently uses de Bruijn syntax), and test which one makes macros easier to write. This would also allow a proper performance evaluation to see the effect of the variable representation on the performance of syntax transformations. And of course my (not so) secret goal is to eventually use one of these representations for the definition of Agda Core!

I’m very curious to hear your thoughts about this overview, whether I have missed any important criteria in this comparison, whether I have seriously misrepresented some of the approaches, whether I skipped one completely. In any of these cases, please let me know via Zulip, Twitter, or mail.