------------------------------------------------------------------------- ----- SIMPLE, GENERIC, TYPE-SAFE SUBSTITUTION IN AGDA ----- ----- Michael Arntzenius , January 2019 ----- ----- ----- ----- Accompanying web page: ----- ----- http://www.rntz.net/post/2019-01-21-generic-substitution.html ----- ----- ----- ----- See also: ----- ----- http://www.rntz.net/post/2019-01-18-binding-in-agda.html ----- ------------------------------------------------------------------------- -- Formalizing substitution in Agda can get tedious if you need a case for every -- term former in your language. In this file 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[1], 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. -- -- [1] http://www.rntz.net/post/2019-01-18-binding-in-agda.html -- and http://www.rntz.net/files/Syntax.agda -- -- 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[2] like LF and Twelf[3], but premise signatures are much simpler -- and less powerful than LF's syntax representation. -- -- [2] https://en.wikipedia.org/wiki/Logical_framework -- [3] http://twelf.org/wiki/Main_Page -- -- Without further ado, let's read some Agda! First, the 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 (see [1] above): 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 typing context of the -- conclusion 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 lambdas. -- -- Γ ⊢ M : A Γ ⊢ N : B Γ,x:A ⊢ M : B -- ────────────────────── pair ───────────────── lambda -- Γ ⊢ (M,N) : A × B Γ ⊢ λ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. 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: -- (#1) x : unit ⊢ x : unit ex1-var : singleton unit ⊢ term unit ex1-var = var refl -- (#2) ∅ ⊢ λx.x : unit => unit ex2-lam : ∅ ⊢ term (unit => unit) ex2-lam = lam ! bind (var (inj₁ refl)) -- (#3) x : unit ⊢ (x,()) : unit × unit ex3-pair : singleton unit ⊢ term (unit × unit) ex3-pair = pair ! var refl , (duh ! tt) -- (#4) ∅ ⊢ 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.