[A well-typed definition of the simply typed lambda calculus.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310040028
 + Includes a simple semantics and a normaliser which uses NBE.
 + No proofs, but everything is well-typed and structurally recursive.
] {
adddir ./SimplyTyped
addfile ./SimplyTyped/ContextExtension.agda
hunk ./SimplyTyped/ContextExtension.agda 1
+------------------------------------------------------------------------
+-- Context extensions
+------------------------------------------------------------------------
+
+module SimplyTyped.ContextExtension where
+
+open import SimplyTyped.TypeSystem
+open import Logic
+open import Relation.Binary.PropositionalEquality
+
+infixl 20 _++_
+
+-- Context extension.
+
+_++_ : Ctxt -> Ctxt -> Ctxt
+Γ ++ ε        = Γ
+Γ ++ (Γ' ▻ τ) = (Γ ++ Γ') ▻ τ
+
+-- Context extension is associative.
+
+++-assoc : forall Γ Δ X -> Γ ++ (Δ ++ X) ≡ (Γ ++ Δ) ++ X
+++-assoc Γ Δ ε       = ≡-refl
+++-assoc Γ Δ (X ▻ σ) = ≡-cong (\Γ -> Γ ▻ σ) (++-assoc Γ Δ X)
addfile ./SimplyTyped/Environment.agda
hunk ./SimplyTyped/Environment.agda 1
+------------------------------------------------------------------------
+-- Environments
+------------------------------------------------------------------------
+
+open import SimplyTyped.TypeSystem
+
+module SimplyTyped.Environment (Contents : Ty -> Set) where
+
+infixl 20 _▷_
+
+data Env : Ctxt -> Set where
+  ∅   : Env ε
+  _▷_ : forall {Γ τ} -> Env Γ -> Contents τ -> Env (Γ ▻ τ)
+
+lookup : forall {Γ τ} -> Γ ∋ τ -> Env Γ -> Contents τ
+lookup vz     (ρ ▷ v) = v
+lookup (vs x) (ρ ▷ v) = lookup x ρ
addfile ./SimplyTyped/Model.agda
hunk ./SimplyTyped/Model.agda 1
+------------------------------------------------------------------------
+-- Models
+------------------------------------------------------------------------
+
+-- Note: I don't think I have included all the laws that these
+-- structures need to satisfy in order to be models. I should probably
+-- have called them "applicative structures" instead.
+
+module SimplyTyped.Model where
+
+open import SimplyTyped.TypeSystem
+
+-- A simple kind of model.
+
+record Model : Set1 where
+  field
+    -- Semantic domains.
+
+    Dom : Ctxt -> Ty -> Set
+
+    -- Interpretations of variables, abstractions and applications.
+
+    Var : forall {Γ τ} -> Γ ∋ τ -> Dom Γ τ
+    Lam : forall {Γ σ τ} -> Dom (Γ ▻ σ) τ -> Dom Γ (σ → τ)
+    App : forall {Γ σ τ} -> Dom Γ (σ → τ) -> Dom Γ σ -> Dom Γ τ
+
+  -- Given a model a term can easily be interpreted:
+
+  ⟦_⟧ : forall {Γ τ} -> Γ ⊢ τ -> Dom Γ τ
+  ⟦ var x   ⟧ = Var x
+  ⟦ λ t     ⟧ = Lam ⟦ t ⟧
+  ⟦ t₁ · t₂ ⟧ = App ⟦ t₁ ⟧ ⟦ t₂ ⟧
addfile ./SimplyTyped/NormalForm.agda
hunk ./SimplyTyped/NormalForm.agda 1
+------------------------------------------------------------------------
+-- Normal forms
+------------------------------------------------------------------------
+
+module SimplyTyped.NormalForm where
+
+open import SimplyTyped.TypeSystem
+open import SimplyTyped.Substitution
+open VarSubst
+
+-- Long βη-normal forms, defined using neutral and normal forms.
+
+infixl 70 _·ⁿ_
+infix  50 λⁿ_
+
+mutual
+
+  data Ne : Ctxt -> Ty -> Set where
+    varⁿ : forall {Γ τ} -> Γ ∋ τ -> Ne Γ τ
+    _·ⁿ_ : forall {Γ σ τ} -> Ne Γ (σ → τ) -> NF Γ σ -> Ne Γ τ
+
+  data NF : Ctxt -> Ty -> Set where
+    ne  : forall {Γ τ} -> Ne Γ τ -> NF Γ τ
+    λⁿ_ : forall {Γ σ τ} -> NF (Γ ▻ σ) τ -> NF Γ (σ → τ)
+
+-- Applying substitutions to normal forms.
+
+infix 48 _[_]ⁿ _[_]ⁿ'
+
+mutual
+
+  _[_]ⁿ' : forall {Γ Δ τ} -> Ne Γ τ -> Γ ⇒ Δ -> Ne Δ τ
+  varⁿ x   [ ρ ]ⁿ' = varⁿ (lookup x ρ)
+  t₁ ·ⁿ t₂ [ ρ ]ⁿ' = (t₁ [ ρ ]ⁿ') ·ⁿ (t₂ [ ρ ]ⁿ)
+
+  _[_]ⁿ : forall {Γ Δ τ} -> NF Γ τ -> Γ ⇒ Δ -> NF Δ τ
+  ne t [ ρ ]ⁿ = ne (t [ ρ ]ⁿ')
+  λⁿ t [ ρ ]ⁿ = λⁿ (t [ ρ ↑ ]ⁿ)
+
+-- Structure-preserving conversion to terms.
+
+mutual
+
+  neToTm : forall {Γ τ} -> Ne Γ τ -> Γ ⊢ τ
+  neToTm (varⁿ x)   = var x
+  neToTm (t₁ ·ⁿ t₂) = neToTm t₁ · nfToTm t₂
+
+  nfToTm : forall {Γ τ} -> NF Γ τ -> Γ ⊢ τ
+  nfToTm (ne t) = neToTm t
+  nfToTm (λⁿ t) = λ nfToTm t
addfile ./SimplyTyped/Normalisation.agda
hunk ./SimplyTyped/Normalisation.agda 1
+------------------------------------------------------------------------
+-- Normalisation
+------------------------------------------------------------------------
+
+module SimplyTyped.Normalisation where
+
+open import SimplyTyped.TypeSystem
+open import SimplyTyped.NormalForm
+open import SimplyTyped.Model
+open import SimplyTyped.Value
+open ValSubst
+
+-- Normalisation.
+
+nf : forall {Γ τ} -> Γ ⊢ τ -> NF Γ τ
+nf t = reify _ (⟦ t ⟧ idˢ)
+  where open Model valModel
addfile ./SimplyTyped/Semantics.agda
hunk ./SimplyTyped/Semantics.agda 1
+------------------------------------------------------------------------
+-- A simple semantics
+------------------------------------------------------------------------
+
+module SimplyTyped.Semantics where
+
+open import SimplyTyped.TypeSystem
+import SimplyTyped.Environment
+open import Data.Nat
+open import SimplyTyped.Model
+
+-- Semantic domains for types.
+
+⟦_⟧⋆ : Ty -> Set
+⟦ Nat   ⟧⋆ = ℕ
+⟦ σ → τ ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆
+
+open SimplyTyped.Environment ⟦_⟧⋆
+
+-- Model.
+
+model : Model
+model = record
+  { Dom = \Γ τ -> Env Γ -> ⟦ τ ⟧⋆
+  ; Var = lookup
+  ; Lam = \f ρ v -> f (ρ ▷ v)
+  ; App = \f x ρ -> f ρ (x ρ)
+  }
+
+module ForIllustrationOnly where
+
+  -- The model above may be hard to grasp at first. If the
+  -- interpretation function is written out explicitly we get the
+  -- following:
+
+  ⟦_⟧ : forall {Γ τ} -> Γ ⊢ τ -> Env Γ -> ⟦ τ ⟧⋆
+  ⟦ var x   ⟧ ρ = lookup x ρ
+  ⟦ λ t     ⟧ ρ = \v -> ⟦ t ⟧ (ρ ▷ v)
+  ⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ (⟦ t₂ ⟧ ρ)
addfile ./SimplyTyped/Substitution.agda
hunk ./SimplyTyped/Substitution.agda 1
+------------------------------------------------------------------------
+-- Substitutions
+------------------------------------------------------------------------
+
+module SimplyTyped.Substitution where
+
+open import SimplyTyped.TypeSystem
+open import SimplyTyped.ContextExtension
+import SimplyTyped.Environment as Env
+open import Data.Function
+
+------------------------------------------------------------------------
+-- General substitution machinery
+
+-- Uses idea from "Type-Preserving Renaming and Substitution" by Conor
+-- McBride to enable defining both term and variable substitutions
+-- without having to write several functions which traverse terms.
+
+-- Definition of what a substitution is.
+
+module SubstDef (_•_ : TmLike) -- The substitution replaces variables
+                               -- with this kind of "term".
+                where
+
+  -- Substitutions of type Γ ⇒ Δ, when applied, take things with
+  -- variables in Γ and give things with variables in Δ. (This concept
+  -- is sometimes written with the arrow in the other direction.)
+
+  -- Substitutions are defined in terms of environments.
+
+  infix 10 _⇒_
+
+  private
+    module Dummy {Δ : Ctxt} where
+      open Env (_•_ Δ) public
+  open Dummy public using (∅; _▷_; lookup)
+
+  _⇒_ : Ctxt -> Ctxt -> Set
+  Γ ⇒ Δ = Dummy.Env {Δ} Γ
+
+  -- The type of functions applying substitutions to things.
+
+  Applier : TmLike -> TmLike -> Set
+  Applier _•₁_ _•₂_ = forall {Γ Δ τ} -> Γ •₁ τ -> Γ ⇒ Δ -> Δ •₂ τ
+
+  -- You get lots of substitution machinery defined for you (see
+  -- below) if you define a SubstKit, ...
+
+  record SubstKit : Set where
+    field
+      vr     :  forall {Γ τ}   -> Γ ∋ τ -> Γ • τ
+      weaken :  forall {Γ σ τ} -> Γ • τ -> Γ ▻ σ • τ
+      tm     :  forall {Γ τ}   -> Γ • τ -> Γ ⊢ τ
+
+  -- ...and more if you define a SubstKit⁺.
+
+  record SubstKit⁺ : Set where
+    field
+      kit  : SubstKit
+      _/•_ : Applier _•_ _•_
+
+open SubstDef using (SubstKit; SubstKit⁺)
+
+-- Various substitution-related functions.
+
+module Subst {_•_ : TmLike}
+             (kit : SubstKit _•_)
+             where
+
+  open SubstDef _•_ public
+  open SubstKit kit
+
+  infix  70 _↑
+  infix  48 _[_]
+
+  -- Weakening of substitutions.
+
+  wk⇒ : forall {Γ Δ σ} -> Γ ⇒ Δ -> Γ ⇒ Δ ▻ σ
+  wk⇒ ∅       = ∅
+  wk⇒ (ρ ▷ t) = wk⇒ ρ ▷ weaken t
+
+  -- Lifting of substitutions.
+
+  _↑ : forall {Γ Δ σ} -> Γ ⇒ Δ -> Γ ▻ σ ⇒ Δ ▻ σ
+  ρ ↑ = wk⇒ ρ ▷ vr vz
+
+  -- Identity.
+
+  idˢ : forall {Γ} -> Γ ⇒ Γ
+  idˢ {Γ = ε}     = ∅
+  idˢ {Γ = Γ ▻ τ} = idˢ ↑
+
+  -- Weakening.
+
+  wk : forall {Γ σ} -> Γ ⇒ Γ ▻ σ
+  wk = wk⇒ idˢ
+
+  -- Substitution of a single variable.
+
+  sub : forall {Γ τ} -> Γ • τ -> Γ ▻ τ ⇒ Γ
+  sub t = idˢ ▷ t
+
+  -- Substitution application for terms.
+
+  _[_] : Applier _⊢_ _⊢_
+  var x   [ ρ ] = tm (lookup x ρ)
+  λ t     [ ρ ] = λ (t [ ρ ↑ ])
+  t₁ · t₂ [ ρ ] = (t₁ [ ρ ]) · (t₂ [ ρ ])
+
+  -- Multiple weakenings.
+
+  wk⇒⋆ : forall {Γ Δ} Δ' -> Γ ⇒ Δ -> Γ ⇒ Δ ++ Δ'
+  wk⇒⋆ ε        ρ = ρ
+  wk⇒⋆ (Δ' ▻ σ) ρ = wk⇒ (wk⇒⋆ Δ' ρ)
+
+  wk⋆ : forall {Γ} Γ' -> Γ ⇒ Γ ++ Γ'
+  wk⋆ Γ' = wk⇒⋆ Γ' idˢ
+
+-- Subst⁺ defines composition. This function uses a stronger
+-- substitution kit, which is sometimes defined using the Subst module
+-- (see the examples below); this is the reason for placing
+-- composition in a separate module.
+
+module Subst⁺ {_•_  : TmLike}
+              (kit⁺ : SubstKit⁺ _•_)
+              where
+
+  open SubstDef.SubstKit⁺ _•_ kit⁺
+  open Subst kit public
+
+  infixl 70 _∘ˢ_
+
+  _∘ˢ_ : forall {Γ Δ X} -> Γ ⇒ Δ -> Δ ⇒ X -> Γ ⇒ X
+  ∅        ∘ˢ ρ₂ = ∅
+  (ρ₁ ▷ t) ∘ˢ ρ₂ = ρ₁ ∘ˢ ρ₂ ▷ (t /• ρ₂)
+
+------------------------------------------------------------------------
+-- Instantiations of the general structures above
+
+-- Variables.
+
+varKit : SubstKit _∋_
+varKit = record
+  { vr     = id
+  ; weaken = vs
+  ; tm     = var
+  }
+
+varKit⁺ : SubstKit⁺ _∋_
+varKit⁺ = record { kit  = varKit
+                 ; _/•_ = Subst.lookup varKit
+                 }
+
+module VarSubst where
+  open Subst⁺ varKit⁺ public
+
+-- Terms.
+
+tmKit : SubstKit _⊢_
+tmKit = record
+  { vr     = var
+  ; weaken = \t -> t [ wk ]
+  ; tm     = id
+  }
+  where open VarSubst
+
+tmKit⁺ : SubstKit⁺ _⊢_
+tmKit⁺ = record { kit  = tmKit
+                ; _/•_ = Subst._[_] tmKit
+                }
+
+module TmSubst where
+  open Subst⁺ tmKit⁺ public
addfile ./SimplyTyped/TypeSystem.agda
hunk ./SimplyTyped/TypeSystem.agda 1
+------------------------------------------------------------------------
+-- The type system of the simply type lambda calculus
+------------------------------------------------------------------------
+
+module SimplyTyped.TypeSystem where
+
+infixl 70 _·_
+infix  50 λ_
+infixr 30 _→_
+infixl 20 _▻_
+infix  10 _∋_ _⊢_
+
+-- Types. (Nat could easily be exchanged for an arbitrary base type.)
+
+data Ty : Set where
+  Nat : Ty
+  _→_ : Ty -> Ty -> Ty
+
+-- Contexts.
+
+data Ctxt : Set where
+  -- Empty context.
+  ε   : Ctxt
+  -- Extension of the context with one more type.
+  _▻_ : Ctxt -> Ty -> Ctxt
+
+-- An abbreviation.
+
+TmLike : Set1
+TmLike = Ctxt -> Ty -> Set
+
+-- Variables (de Bruijn indices).
+
+data _∋_ : TmLike where
+  -- Zero.
+  vz : forall {Γ σ}   -> Γ ▻ σ ∋ σ
+  -- Successor.
+  vs : forall {Γ σ τ} -> Γ ∋ τ -> Γ ▻ σ ∋ τ
+
+-- Terms.
+
+data _⊢_ : TmLike where
+  var  : forall {Γ τ}   -> Γ ∋ τ -> Γ ⊢ τ
+  λ_   : forall {Γ σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ → τ
+  _·_  : forall {Γ σ τ} -> Γ ⊢ σ → τ -> Γ ⊢ σ -> Γ ⊢ τ
addfile ./SimplyTyped/Value.agda
hunk ./SimplyTyped/Value.agda 1
+------------------------------------------------------------------------
+-- Values
+------------------------------------------------------------------------
+
+module SimplyTyped.Value where
+
+open import SimplyTyped.TypeSystem
+open import SimplyTyped.NormalForm
+open import SimplyTyped.Substitution
+open import SimplyTyped.ContextExtension
+open import SimplyTyped.Model
+open import Data.Function
+open import Relation.Binary.PropositionalEquality
+
+-- Values.
+
+Val : Ctxt -> Ty -> Set
+Val Γ Nat     = Ne Γ Nat
+Val Γ (σ → τ) = forall Γ' -> Val (Γ ++ Γ') σ -> Val (Γ ++ Γ') τ
+
+-- Semantic application.
+
+infixl 70 _·ˢ_
+
+_·ˢ_ : forall {Γ σ τ} -> Val Γ (σ → τ) -> Val Γ σ -> Val Γ τ
+f ·ˢ x = f ε x
+
+-- Reflection and reification.
+
+mutual
+
+  reflect : forall {Γ} τ -> Ne Γ τ -> Val Γ τ
+  reflect Nat     t = t
+  reflect (σ → τ) t = \Γ' v -> reflect τ ((t [ wk⋆ Γ' ]ⁿ') ·ⁿ reify σ v)
+    where open VarSubst
+
+  reify : forall {Γ} τ -> Val Γ τ -> NF Γ τ
+  reify Nat     t = ne t
+  reify (σ → τ) f = λⁿ (reify τ (f (ε ▻ σ) (reflect σ (varⁿ vz))))
+
+-- Weakening.
+
+wkˢ : forall {Γ} τ Γ' -> Val Γ τ -> Val (Γ ++ Γ') τ
+wkˢ Nat Γ' t = t [ wk⋆ Γ' ]ⁿ'
+  where open VarSubst
+wkˢ {Γ} (σ → τ) Γ' f = \Γ'' v ->
+  let cast₁ = ≡-subst (\Γ -> Val Γ σ) (≡-sym $ ++-assoc Γ Γ' Γ'')
+      cast₂ = ≡-subst (\Γ -> Val Γ τ) (++-assoc Γ Γ' Γ'')
+  in cast₂ (f (Γ' ++ Γ'') (cast₁ v))
+
+-- Value substitutions.
+
+open SubstDef using (SubstKit)
+
+valKit : SubstKit Val
+valKit = record
+  { vr     = reflect _ ∘ varⁿ
+  ; weaken = wkˢ _ (ε ▻ _)
+  ; tm     = nfToTm ∘ reify _
+  }
+
+module ValSubst where
+  open Subst valKit public
+
+open ValSubst
+
+-- A model using these values.
+
+valModel : Model
+valModel = record
+  { Dom = \Γ τ -> forall {Δ} -> Γ ⇒ Δ -> Val Δ τ
+  ; Var = \x ρ -> lookup x ρ
+  ; Lam = \f ρ Δ' v -> f (wk⇒⋆ Δ' ρ ▷ v)
+  ; App = \v₁ v₂ ρ -> v₁ ρ ·ˢ v₂ ρ
+  }
+
+module ForIllustrationOnly where
+
+  -- The evaluation function that you get from this model:
+
+  ⟦_⟧ : forall {Γ Δ τ} -> Γ ⊢ τ -> Γ ⇒ Δ -> Val Δ τ
+  ⟦ var x   ⟧ ρ = lookup x ρ
+  ⟦ λ t     ⟧ ρ = \Δ' v -> ⟦ t ⟧ (wk⇒⋆ Δ' ρ ▷ v)
+  ⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ ·ˢ ⟦ t₂ ⟧ ρ
}