--------------------------------------------------------------------
----- REPRESENTING BINDING IN AGDA USING CONTEXTS AS FUNCTIONS -----
----- Michael Arntzenius , January 2019 -----
----- -----
----- Accompanying web page: -----
----- http://www.rntz.net/post/2019-01-18-binding-in-agda.html -----
--------------------------------------------------------------------
-- 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.
-- I've since learned 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.
-- 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. The only interesting bit is
-- 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. This is easily done by using renaming
-- to weaken all the terms in our substitution. 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 S4, but I do not see any good way to extend it
-- to handle linear or dependent type systems.