STLC.agda

module STLC where

-- Simple substitution à la Conor, as described in http://strictlypositive.org/ren-sub.pdf

id : {A : Set} → A → A
id x = x

data Type : Set where
  *   : Type
  _⇒_ : (S T : Type) → Type

data Context : Set where
  ε   : Context
  _,_ : (Γ : Context) (S : Type) → Context

data _∋_ : Context → Type → Set where
  here  : ∀ {Γ S} → (Γ , S) ∋ S
  there : ∀ {Γ S T} (i : Γ ∋ S) → (Γ , T) ∋ S

data Term : Context → Type → Set where
  var : ∀ {Γ S} (v : Γ ∋ S) → Term Γ S
  lam : ∀ {Γ S T} (t : Term (Γ , S) T) → Term Γ (S ⇒ T)
  app : ∀ {Γ S T} (f : Term Γ (S ⇒ T)) (x : Term Γ S) → Term Γ T

record Kit (_◆_ : Context → Type → Set) : Set where
  constructor kit
  field
    variable : ∀ {Γ T}   → Γ ∋ T → Γ ◆ T
    term     : ∀ {Γ T}   → Γ ◆ T → Term Γ T
    weaken   : ∀ {Γ S T} → Γ ◆ T → (Γ , S) ◆ T

open Kit

lift : ∀ {Γ Δ S T _◆_} → Kit _◆_ → (∀ {X} → Γ ∋ X → Δ ◆ X) → (Γ , S) ∋ T → (Δ , S) ◆ T
lift K τ here      = variable K here
lift K τ (there v) = weaken K (τ v)

traverse : ∀ {Γ Δ T _◆_} → Kit _◆_ → (∀ {X} → Γ ∋ X → Δ ◆ X) → Term Γ T → Term Δ T
traverse K τ (var v)   = term K (τ v)
traverse K τ (lam t)   = lam (traverse K (lift K τ) t)
traverse K τ (app f x) = app (traverse K τ f) (traverse K τ x)


rename : ∀ {Γ Δ T} → (∀ {X} → Γ ∋ X → Δ ∋ X) → Term Γ T → Term Δ T
rename p t = traverse (kit id var there) p t

subst : ∀ {Γ Δ T} → (∀ {X} → Γ ∋ X → Term Δ X) → Term Γ T → Term Δ T
subst σ t = traverse (kit var id (rename there)) σ t

subst₁ : ∀ {Γ S T} → Term Γ S → Term (Γ , S) T → Term Γ T
subst₁ {Γ} {S} t = subst f
  where
  f : ∀ {X} → (Γ , S) ∋ X → Term Γ X
  f here = t
  f (there x) = var x


data Env : Context → Set where
  ε   : Env ε
  _,_ : ∀ {Γ T} (xs : Env Γ) (x : Term Γ T) → Env (Γ , T)

-- World's slowest full substitution
subst′ : ∀ {Γ T} → Env Γ → Term Γ T → Term ε T
subst′ ε t = t
subst′ (xs , x) t = subst′ xs (subst₁ x t)