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
field
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
field
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
{-# NO_POSITIVITY_CHECK #-}
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)
)
)
where
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
field
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
field
-- 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
field
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)))
where
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.
instance
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
variable
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
variable
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:
First-order representation: does the representation avoid the use of meta-level functions as part of the data structure? If not, it can be difficult or impossible to do things like checking equality of terms or pretty-printing.
Named variables: When I write down a piece of syntax, are variables represented by their names or anonymously? This provides some measure of readability by humans.
Enforces α-equivalence: Does the representation enforce that two α-equivalent terms are treated in the same way?
Enforces well-scopedness: Does the representation enforce that names can only be used when they are in fact in scope?
No mixing of scopes: Does the representation enforce that a name that comes from one scope is not used in a different scope?
Abstract interface: Does the representation provide an abstract interface that can be instantiated in different ways?
Enforces freshness: Does the representation allow us to require that names must be fresh at certain positions in the syntax?
Strengthening is no-op: Can we remove unused names from the scope without having to change the syntax?
So here’s the full table:
| Bare | DeBr | LoNa | Nom | PHOAS | WTDB | WTDB+N | FreshL | NaPa | ASG | NomPa | CoDB | CoDB+N | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 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.