-------------------------------------------------------------------------
----- 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.