[Included an infinite set of base types.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080310040440] {
hunk ./SimplyTyped/Semantics.agda 5
-module SimplyTyped.Semantics where
+open import Data.Nat
+
+module SimplyTyped.Semantics
+         -- Semantic domains of all the base types.
+         (Base : ℕ -> Set)
+         where
hunk ./SimplyTyped/Semantics.agda 14
-open import Data.Nat
hunk ./SimplyTyped/Semantics.agda 19
-⟦ Nat   ⟧⋆ = ℕ
-⟦ σ → τ ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆
+⟦ base n ⟧⋆ = Base n
+⟦ σ → τ  ⟧⋆ = ⟦ σ ⟧⋆ -> ⟦ τ ⟧⋆
hunk ./SimplyTyped/TypeSystem.agda 7
+open import Data.Nat
+
hunk ./SimplyTyped/TypeSystem.agda 15
--- Types. (Nat could easily be exchanged for an arbitrary base type.)
+-- Types.
hunk ./SimplyTyped/TypeSystem.agda 18
-  Nat : Ty
-  _→_ : Ty -> Ty -> Ty
+  base : ℕ -> Ty
+  _→_  : Ty -> Ty -> Ty
hunk ./SimplyTyped/Value.agda 18
-Val Γ Nat     = Ne Γ Nat
-Val Γ (σ → τ) = forall Γ' -> Val (Γ ++ Γ') σ -> Val (Γ ++ Γ') τ
+Val Γ (base n) = Ne Γ (base n)
+Val Γ (σ → τ)  = forall Γ' -> Val (Γ ++ Γ') σ -> Val (Γ ++ Γ') τ
hunk ./SimplyTyped/Value.agda 33
-  reflect Nat     t = t
-  reflect (σ → τ) t = \Γ' v -> reflect τ ((t [ wk⋆ Γ' ]ⁿ') ·ⁿ reify σ v)
+  reflect (base n) t = t
+  reflect (σ → τ)  t = \Γ' v ->
+    reflect τ ((t [ wk⋆ Γ' ]ⁿ') ·ⁿ reify σ v)
hunk ./SimplyTyped/Value.agda 39
-  reify Nat     t = ne t
-  reify (σ → τ) f = λⁿ (reify τ (f (ε ▻ σ) (reflect σ (varⁿ vz))))
+  reify (base n) t = ne t
+  reify (σ → τ)  f = λⁿ (reify τ (f (ε ▻ σ) (reflect σ (varⁿ vz))))
hunk ./SimplyTyped/Value.agda 45
-wkˢ Nat Γ' t = t [ wk⋆ Γ' ]ⁿ'
+wkˢ (base n) Γ' t = t [ wk⋆ Γ' ]ⁿ'
}