[Mirrored the development using PHOAS instead of de Bruijn indices.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080710185538] {
adddir ./HOAS
adddir ./HOAS/SimplyTyped
hunk ./Everything.agda 50
+-- The following modules mirror most of the development above, but use
+-- HOAS (more specifically, Adam Chlipala's PHOAS) instead of
+-- de Bruijn indices.
+
+import HOAS.SimplyTyped.TypeSystem
+import HOAS.SimplyTyped.Evaluation
+import HOAS.SimplyTyped.NormalForm
+import HOAS.SimplyTyped.Value
+import HOAS.SimplyTyped.Normalisation
+
addfile ./HOAS/SimplyTyped/Evaluation.agda
hunk ./HOAS/SimplyTyped/Evaluation.agda 1
+------------------------------------------------------------------------
+-- Evaluating terms
+------------------------------------------------------------------------
+
+open import Data.Nat
+
+module HOAS.SimplyTyped.Evaluation
+         -- Semantic domains of all the base types.
+         (Base : ℕ -> Set)
+         where
+
+open import HOAS.SimplyTyped.TypeSystem
+
+-- Semantic domains for types.
+
+⟦_⟧⋆ : Ty -> Set
+⟦ base n ⟧⋆ = Base n
+⟦ σ → τ  ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆
+
+-- Evaluation.
+
+⟦_⟧' : forall {τ} -> Tm' ⟦_⟧⋆ τ -> ⟦ τ ⟧⋆
+⟦ var x   ⟧' = x
+⟦ λ t     ⟧' = \x -> ⟦ t x ⟧'
+⟦ t₁ · t₂ ⟧' = ⟦ t₁ ⟧' ⟦ t₂ ⟧'
+
+⟦_⟧ : forall {τ} -> Tm τ -> ⟦ τ ⟧⋆
+⟦ t ⟧ = ⟦ t ⟧'
addfile ./HOAS/SimplyTyped/NormalForm.agda
hunk ./HOAS/SimplyTyped/NormalForm.agda 1
+------------------------------------------------------------------------
+-- Normal forms
+------------------------------------------------------------------------
+
+module HOAS.SimplyTyped.NormalForm where
+
+open import HOAS.SimplyTyped.TypeSystem
+
+-- η-long β-normal forms, defined using neutral and normal forms.
+
+infixl 70 _·_
+infix  50 λ_
+
+mutual
+
+  data Ne (V : Ty -> Set) : Ty -> Set where
+    var : forall {τ} (x : V τ) -> Ne V τ
+    _·_ : forall {σ τ} (t₁ : Ne V (σ → τ)) (t₂ : NF' V σ) -> Ne V τ
+
+  data NF' (V : Ty -> Set) : Ty -> Set where
+    ne : forall {n} (t : Ne V (base n)) -> NF' V (base n)
+    λ_ : forall {σ τ} (t : V σ -> NF' V τ) -> NF' V (σ → τ)
+
+NF : Ty -> Set1
+NF σ = forall {V} -> NF' V σ
+
+-- Structure-preserving conversion to terms.
+
+mutual
+
+  neToTm : forall {V τ} -> Ne V τ -> Tm' V τ
+  neToTm (var x)   = var x
+  neToTm (t₁ · t₂) = neToTm t₁ · nfToTm' t₂
+
+  nfToTm' : forall {V τ} -> NF' V τ -> Tm' V τ
+  nfToTm' (ne t) = neToTm t
+  nfToTm' (λ t)  = λ (\x -> nfToTm' (t x))
+
+nfToTm : forall {τ} -> NF τ -> Tm τ
+nfToTm t = nfToTm' t
addfile ./HOAS/SimplyTyped/Normalisation.agda
hunk ./HOAS/SimplyTyped/Normalisation.agda 1
+------------------------------------------------------------------------
+-- Normalisation
+------------------------------------------------------------------------
+
+module HOAS.SimplyTyped.Normalisation where
+
+open import HOAS.SimplyTyped.TypeSystem
+open import HOAS.SimplyTyped.NormalForm
+open import HOAS.SimplyTyped.Value
+
+-- Normalisation.
+
+nf : forall {τ} -> Tm τ -> NF τ
+nf t = reify _ ⟦ t ⟧
addfile ./HOAS/SimplyTyped/TypeSystem.agda
hunk ./HOAS/SimplyTyped/TypeSystem.agda 1
+------------------------------------------------------------------------
+-- The type system of the simply type lambda calculus
+------------------------------------------------------------------------
+
+module HOAS.SimplyTyped.TypeSystem where
+
+open import SimplyTyped.TypeSystem public using (Ty; base; _→_)
+
+infixl 70 _·_
+infix  50 λ_
+
+-- Terms.
+
+data Tm' (V : Ty -> Set) : Ty -> Set where
+  var : forall {σ}   (x : V σ) -> Tm' V σ
+  λ_  : forall {σ τ} (t : V σ -> Tm' V τ) -> Tm' V (σ → τ)
+  _·_ : forall {σ τ} (t₁ : Tm' V (σ → τ)) (t₂ : Tm' V σ) -> Tm' V τ
+
+Tm : Ty -> Set1
+Tm σ = forall {V} -> Tm' V σ
addfile ./HOAS/SimplyTyped/Value.agda
hunk ./HOAS/SimplyTyped/Value.agda 1
+------------------------------------------------------------------------
+-- Values
+------------------------------------------------------------------------
+
+module HOAS.SimplyTyped.Value where
+
+open import HOAS.SimplyTyped.TypeSystem
+open import HOAS.SimplyTyped.NormalForm
+open import Data.Function
+
+-- Values.
+
+Val' : (Ty -> Set) -> Ty -> Set
+Val' V (base n) = Ne V (base n)
+Val' V (σ → τ)  = Val' V σ -> Val' V τ
+
+Val : Ty -> Set1
+Val σ = forall {V} -> Val' V σ
+
+-- Reflection and reification.
+
+mutual
+
+  reflect : forall {V} τ -> Ne V τ -> Val' V τ
+  reflect (base n) t = t
+  reflect (σ → τ)  t = \v -> reflect τ (t · reify σ v)
+
+  reify : forall {V} τ -> Val' V τ -> NF' V τ
+  reify (base n) t = ne t
+  reify (σ → τ)  f = λ (\x -> reify τ (f (reflect σ (var x))))
+
+-- Semantic application.
+
+infixl 70 _·ˢ_
+
+_·ˢ_ : forall {σ τ} -> Val (σ → τ) -> Val σ -> Val τ
+f ·ˢ x = f x
+
+-- Conversions.
+
+varToVal : forall {V τ} -> V τ -> Val' V τ
+varToVal = reflect _ ∘ var
+
+valToTm : forall {τ} -> Val τ -> Tm τ
+valToTm t = nfToTm (reify _ t)
+
+-- Evaluation.
+
+⟦_⟧' : forall {V τ} -> Tm' (Val' V) τ -> Val' V τ
+⟦ var x   ⟧' = x
+⟦ λ t     ⟧' = \v -> ⟦ t v ⟧'
+⟦ t₁ · t₂ ⟧' = ⟦ t₁ ⟧' ⟦ t₂ ⟧'
+
+⟦_⟧ : forall {τ} -> Tm τ -> Val τ
+⟦ t ⟧ = ⟦ t ⟧'
}