-- Solution to type-preserving interpretation using fancier types -- Shin-cheng Mu, 2008 -- http://www.iis.sinica.edu.tw/~scm/2008/typed-lambda-calculus-interprete/ -- Thanks to dependent types, lookup and lookupEnv have no pattern-match -- failure -- Thanks to the type function ⟦_⟧ᵀ and GADT Term, we don't need universal type -- Term expresses all and _only_ well-typed terms in the object language -- I have seen similar code, and the claim that dependent types are -- really needed to express the type system of simply-typed lambda-calculus module Term where open import Data.Nat open import Data.Fin hiding (_+_) open import Data.Vec data TExp : Set where N : TExp _⇒_ : (σ : TExp) → (τ : TExp) → TExp ⟦_⟧ᵀ : TExp → Set ⟦ N ⟧ᵀ = ℕ ⟦ σ ⇒ τ ⟧ᵀ = ⟦ σ ⟧ᵀ → ⟦ τ ⟧ᵀ Cxt : ℕ → Set Cxt n = Vec TExp n data Term {n : ℕ} (Γ : Cxt n) : TExp → Set where val : ∀{σ} → (v : ⟦ σ ⟧ᵀ) → Term Γ σ var : (i : Fin n) → Term Γ (lookup i Γ) _∔_ : (m : Term Γ N) → (n : Term Γ N) → Term Γ N _·_ : ∀{σ τ} → (f : Term Γ (σ ⇒ τ)) → (e : Term Γ σ) → Term Γ τ ƛ : ∀ σ {τ} → (e : Term (σ ∷ Γ) τ) → Term Γ (σ ⇒ τ) data Env : {n : ℕ} → Cxt n → Set where [] : Env [] _∷_ : ∀{σ n}{Γ : Cxt n} → (v : ⟦ σ ⟧ᵀ) → (ρ : Env Γ) → Env (σ ∷ Γ) lookupEnv : ∀ {n}{Γ} → (i : Fin n) → (ρ : Env Γ) → ⟦ lookup i Γ ⟧ᵀ lookupEnv zero (v ∷ ρ) = v lookupEnv (suc i) (_ ∷ ρ) = lookupEnv i ρ ⟦_⟧ : ∀{n}{Γ : Cxt n}{σ} → Term Γ σ → Env Γ → ⟦ σ ⟧ᵀ ⟦ val v ⟧ ρ = v ⟦ var i ⟧ ρ = lookupEnv i ρ ⟦ m ∔ n ⟧ ρ = ⟦ m ⟧ ρ + ⟦ n ⟧ ρ ⟦ f · e ⟧ ρ = ⟦ f ⟧ ρ (⟦ e ⟧ ρ) ⟦ ƛ σ e ⟧ ρ = λ x → ⟦ e ⟧ x ∷ ρ