Representing binding syntax in theorem provers is a chore. For some time now, I've been using a simple yet effective technique to represent binding in Agda. It's far from perfect, but it requires nothing outside the standard library, and makes the metatheory of weakening and substitution fairly simple. Since I hadn't seen anyone else using this particular technique, I thought I'd try explaining it.¹

The basic idea is to use intrinsically typed terms where variables are proofs that a certain type occurs in the context. This is not original. However, rather than the context being a list (or tree, or other data structure) of types, it is a function taking object-language types to meta-language types.

Without further ado, let's look at some Agda code! If you want to follow along in your editor, you can find this entire blog post as an Agda file here. First, some boring set-up:

open import Data.Empty using (⊥)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

infix  1 _⊢_ _⊢⋆_
infixr 4 _∷_ _∪_
infixr 5 _=>_

Now, we come to our object-language's types. We'll consider a simply-typed λ-calculus with a base type, functions, and nothing else.

data Type : Set where
  base : Type
  _=>_ : (A B : Type) -> Type

Now, the core technique. A context is a function mapping object-language types to the collection of variables of that type, represented as a meta-language type ─ in Agda, a Set. The empty context ∅, for example, has no variables of any type, so it always returns ⊥.

Cx : Set1
Cx = Type -> Set

∅ : Cx
∅ _ = ⊥

The (disjoint) union of two contexts is given by their pointwise (disjoint) sum. More plainly, the variables in Γ ∪ Δ of type A are the variables in Γ of type A, plus those in Δ of type A.

_∪_ : (Γ Δ : Cx) → Cx
(Γ ∪ Δ) A = Γ A ⊎ Δ A

A singleton context contains exactly one variable of a particular type, A. So when we're asked what variables it contains of type B, we want a type that has exactly one inhabitant (representing our single variable) if A = B and none otherwise. In other words, propositional equality!

singleton : Type → Cx
singleton A B = A ≡ B

To add a variable to a context, simply union with a new singleton context.

_∷_ : Type → Cx → Cx
A ∷ Γ = singleton A ∪ Γ

Now we can describe the open terms of the simply typed lambda calculus: variables, λs, and applications.

data _⊢_ (Γ : Cx) : (A : Type) → Set where
  var : ∀{A} → Γ A → Γ ⊢ A
  lam : ∀{A B} → A ∷ Γ ⊢ B → Γ ⊢ A => B
  app : ∀{A B} → Γ ⊢ A => B → Γ ⊢ A → Γ ⊢ B

Rather than jumping straight to substitution, I find it simplifies the metatheory to deal with renamings first. By renaming I mean something slightly looser than the usual notion of α-equivalence. A renaming ρ : Γ ⊇ Δ supplies the variables in Δ using variables (not terms!) from Γ. Renamings capture the structural rules of weakening, exchange, and contraction of contexts, without touching more language-specific syntax. Contexts form a category under renamings.

_⊇_ : (Γ Δ : Cx) → Set
Γ ⊇ Δ = ∀{a} → Δ a → Γ a

Applying a renaming to a term is straightforward. When we go under a λ-binder, we have to lift our renaming from Γ ⊇ Δ to A ∷ Γ ⊇ A ∷ Δ, telling it not to molest the λ-bound variable of type A.

rename : ∀{Γ Δ a} → Γ ⊇ Δ → Δ ⊢ a → Γ ⊢ a
rename ρ (var x) = var (ρ x)
rename ρ (lam M) = lam (rename (Data.Sum.map id ρ) M)
rename ρ (app M N) = app (rename ρ M) (rename ρ N)

Now we introduce substitutions. A substitution ρ : Γ ⊢⋆ Δ supplies terms for each variable in Δ; these terms take their variable from Γ. This is sometimes called parallel or simultaneous substitution, since we substitute for all variables in Δ simultaneously. I find formalising this is usually easier than trying to substitute for only one variable at a time. Contexts also form a category under substitutions (of which contexts-with-renamings is a subcategory).

_⊢⋆_ : (Γ Δ : Cx) → Set
Γ ⊢⋆ Δ = ∀{a} → Δ a → Γ ⊢ a

Substitution is quite easy to define. It only needs a lemma, ∪/⊢⋆, that applies a substitution under a binder by weakening the substitution's terms. This corresponds to lifting the context union operator ∪ over a substitution, or as a category theorist would say, that ∪ is a bifunctor over substitutions.

∪/⊢⋆ : ∀{Γ Δ Ψ} → Γ ⊢⋆ Δ → Ψ ∪ Γ ⊢⋆ Ψ ∪ Δ
∪/⊢⋆ σ = [ var ∘ inj₁ , rename inj₂ ∘ σ ]

subst : ∀{Γ Δ a} → Γ ⊢⋆ Δ → Δ ⊢ a → Γ ⊢ a
subst σ (var x) = σ x
subst σ (lam M) = lam (subst (∪/⊢⋆ σ) M)
subst σ (app M N) = app (subst σ M) (subst σ N)

And that's all! I will note briefly that I have extended this technique to handle modal type systems à la Pfenning-Davies S4, but I do not see any good way to extend it to handle linear or dependent type systems.

Footnotes

1. I've since learned from Max New that this technique was taught to students at one of the DeepSpec summer schools. Like many such clever ideas, I'm sure it's been independently discovered several times, but I'm still interested in where it originated; feel free to shoot me an email. ↩