Simple, generic, type-safe substitution in Agda

Formalizing substitution in Agda can get tedious if you need a case for every term former in your language. In this post I show how to avoid this tedium by implementing substitution generically. However, the technique I present is limited to simple type systems for λ-calculi, and does not handle polymorphism, linearity, dependence, sequent calculi, or other fancy stuff.

For lack of a better name, I call this technique premise signatures. Previously, I also showed how to encode binders in Agda by using functions as contexts. In principle these techniques are independent, but they work well together, so I will assume you have read my previous post and use functions as contexts here without explanation.

I haven't seen anyone else use premise signatures. I'd love to know if I'm reinventing a well-known technique. It reminds me a little of logical frameworks like LF and Twelf, but premise signatures are much simpler and less powerful than LF's syntax representation.

Without further ado, let's read some Agda! 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.Bool using (Bool; true; false; if_then_else_)
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 2 _∧_
infixr 3 _▷_
infixr 4 _∷_ _∪_ _!_
infixr 5 _=>_ _,_
infixr 6 _×_ _+_

Our type language will be richer this time, to demonstrate that adding features to the language won't complicate our definition of substitution.

data Type : Set where
  void unit : Type
  _=>_ _×_ _+_ : (A B : Type) -> Type

We use functions as contexts:

Cx : Set1
Cx = Type -> Set

∅ : Cx
∅ _ = ⊥

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

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

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

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

Now we come to the meat of the subject. A value of type Sig ─ a premise signature ─ represents the types of the arguments to a term former, or equivalently, the premises of a particular typing rule.

data Sig : Set1 where
  -- No arguments/premises.
  nil : Sig

  -- A pair of arguments or conjunction of premises.
  _∧_ : (P Q : Sig) → Sig

  -- A binder; a premise P beneath a context Γ of newly
  -- bound variables.
  _▷_ : (Γ : Cx) (P : Sig) → Sig

  -- A term of a given type.
  term : (A : Type) → Sig

Note that in term, we don't provide a context; the conclusion's typing context is implicitly threaded through all premises. This is the crucial choice that lets substitution be implemented generically. It's also why this particular definition of Sig can't handle linear or modal logics.

For example, let's consider the rules for pairs and functions.

Γ ⊢ M : A   Γ ⊢ N : B
────────────────────── pair
 Γ ⊢ (M,N) : A × B

 Γ,x:A ⊢ M : B
───────────────── lambda
Γ ⊢ λx.M : A → B

We can represent these rules' premises like so:

pair-premise λ-premise : (A B : Type) → Sig
pair-premise A B = term A ∧ term B  
λ-premise A B = singleton A ▷ term B

Note that we aren't representing whole rules here, just their premises. To represent a typing rule, we also need its conclusion. For our purposes, the conclusion of a typing rule is characterized by the type of the term it produces; the context is left implicit. We represent inference rules, or term formers, as constructors of the type P ⊩ A, where P is the premise signature and A the type of the conclusion, i.e. of the term formed. To demonstrate that our definition of substitution really is generic, we'll encode a moderately complex term syntax:

data _⊩_ : Sig → Type → Set where
  lam : ∀{A B} → singleton A ▷ term B ⊩ A => B
  app : ∀{A B} → term (A => B) ∧ term A ⊩ B
  pair : ∀{A B} → term A ∧ term B ⊩ A × B
  proj : ∀{A B} (left : Bool)
      → term (A × B) ⊩ (if left then A else B)
  inj : ∀{A B} (left : Bool)
      → term (if left then A else B) ⊩ A + B
  case : ∀{A B C}
       → term (A + B)
         ∧ singleton A ▷ term C
         ∧ singleton B ▷ term C
         ⊩ C
  duh : nil ⊩ unit            -- unit introduction
  wat : ∀{A} → term void ⊩ A  -- void elimination
  -- General recursion at any type, because why not?
  fix : ∀{A} → singleton A ▷ term A ⊩ A

Now, at last, we can define the type of well-typed terms in a given context. In fact, we'll do more than that: we'll define the type of well-typed arguments to a term former ─ in other words, of proofs of the premises of an inference rule.

data _⊢_ (Γ : Cx) : (P : Sig) → Set1 where
  -- It's easy to prove nothing.
  tt : Γ ⊢ nil

  -- To prove a pair of premises, prove them both.
  _,_ : ∀{P Q} → Γ ⊢ P → Γ ⊢ Q → Γ ⊢ P ∧ Q

  -- To prove something under a binder, introduce new
  -- variables to the context.
  bind : ∀{Δ P} → Δ ∪ Γ ⊢ P → Γ ⊢ Δ ▷ P

  -- To supply a term of type A, use a term former and
  -- prove its premises.
  _!_ : ∀{P A} (form : P ⊩ A) (args : Γ ⊢ P) → Γ ⊢ term A

  -- Or, you can use a variable from the context.
  var : ∀{A} → Γ A → Γ ⊢ term A

Let's see some examples of terms written in this syntax:

-- x : unit ⊢ x : unit
ex1-var : singleton unit ⊢ term unit
ex1-var = var refl

-- ∅ ⊢ λx.x : unit => unit
ex2-lam : ∅ ⊢ term (unit => unit)
ex2-lam = lam ! bind (var (inj₁ refl))

-- x : unit ⊢ (x,()) : unit × unit
ex3-pair : singleton unit ⊢ term (unit × unit)
ex3-pair = pair ! var refl , (duh ! tt)

-- ∅ ⊢ fix x. x : A
ex4-rec : (A : Type) → ∅ ⊢ term A
ex4-rec A = fix ! bind (var (inj₁ refl))

Okay, now that we have our notion of term syntax (or, I suppose, term former argument syntax), let's implement renaming for it. This follows the same pattern seen in my earlier article.

rename : ∀{Γ Δ P} → Γ ⊇ Δ → Δ ⊢ P → Γ ⊢ P
rename σ tt = tt
rename σ (M , N) = rename σ M , rename σ N
rename σ (bind M) = bind (rename (Data.Sum.map id σ) M)
rename σ (form ! M) = form ! rename σ M
rename σ (var x) = var (σ x)

Note that we never had to mention any of our term formers! Okay, but maybe that was just a fluke. Let's move on to simultaneous substitutions.

_⊢⋆_ : (Γ Δ : Cx) → Set1
Γ ⊢⋆ Δ = ∀{a : Type} → Δ a → Γ ⊢ term a

Again, we need a lemma for substituting under a binder that leaves the newly bound variable(s) alone:

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

Finally, substitution:

subst : ∀{Γ Δ P} → Γ ⊢⋆ Δ → Δ ⊢ P → Γ ⊢ P
subst σ tt = tt
subst σ (P , Q) = subst σ P , subst σ Q
subst σ (bind P) = bind (subst (∪/⊢⋆ σ) P)
subst σ (form ! P) = form ! subst σ P
subst σ (var x) = σ x

As in rename, there is no mention of either types or term formers: we don't need individual cases for lam, app, pair, proj, fix, etc. This is a generic implementation of type-safe substitution for any simple type theory!

This generality should not be overstated, however. I have managed to extend this technique to handle a modal type theory similar to Pfenning-Davies S4, but not to polymorphic, linear, or dependent types. It's also specific to λ-calculi (or natural deduction style) rather than sequent calculi; it cannot represent rules that analyse the types in the context.