module Talk where

{-

James Chapman

Time Based Art (TBA)

Theory Days at Otepää, Feb 3 2013

Acknowledgements: Kurt Gödel, William Tait, and Per Martin-Löf

-}

-- import def of natural numbers and pragma that allows us to write 0,1, etc.
open import Data.Nat hiding (_<_)

-- codes for types
data Ty : Set where
  nat : Ty
  _⇒_ : Ty → Ty → Ty

-- contexts are lists of types
data Con : Set where
  ε   : Con
  _<_ : Con → Ty → Con

-- well typed variables, de Bruijn indices (just natural numbers)
data Var : Con → Ty → Set where
  zero : ∀{Γ σ} → Var (Γ < σ) σ
  suc  : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ

-- well typed terms of lambda calculus + zero, suc and a primitive recursion operator
data Tm : Con → Ty → Set where
  var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
  lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)
  app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
  zero : ∀{Γ} → Tm Γ nat
  suc : ∀{Γ} → Tm Γ nat → Tm Γ nat
  prim : ∀{Γ σ} → Tm Γ nat → Tm Γ σ → Tm Γ (σ ⇒ σ) → Tm Γ σ

-- the meaning of/decoding for types
Val : Ty → Set
Val nat      = ℕ
Val (σ ⇒ σ₁) = Val σ → Val σ₁

-- meaning of/decoder for contexts
Env : Con → Set
Env Γ = {σ : _} → Var Γ σ → Val σ

-- environment extension
_<'_ : ∀{Γ σ} → Env Γ → Val σ → Env (Γ < σ)
(γ <' v) zero = v
(γ <' v) (suc x) = γ x

-- primrec operator on 'values'
vprim : {X : Set} → ℕ → X → (X → X) → X
vprim zero z f = z
vprim (suc n) z f = f (vprim n z f)

-- meaning of terms/decoder
-- the meaning of a Tm Γ σ is a function from environments over Γ to values of type σ
⟦_⟧ : ∀{Γ σ} → Tm Γ σ → (Env Γ → Val σ)
⟦ var x      ⟧ γ = γ x
⟦ lam t      ⟧ γ = λ v → ⟦ t ⟧ (γ <' v)
⟦ app t u    ⟧ γ = ⟦ t ⟧ γ (⟦ u ⟧ γ)
⟦ zero       ⟧ γ = 
⟦ suc t      ⟧ γ =  + (⟦ t ⟧ γ)
⟦ prim t z f ⟧ γ = vprim (⟦ t ⟧ γ) (⟦ z ⟧ γ) (⟦ f ⟧ γ)

-- the number 2 as a term
two : ∀{Γ} → Tm Γ nat
two = suc (suc zero)

-- the addition function as a term
plus : ∀{Γ} → Tm Γ (nat ⇒ (nat ⇒ nat))
plus = lam (lam (prim (var (suc zero)) (var zero) (lam (suc (var zero)))))

-- '2 + 2' as a term
example : ∀{Γ} → Tm Γ nat
example = app (app plus two) two

-- the empty environment (there are no variables in the empty environment)
empty : Env ε
empty ()

-- '2 + 2' evaluated
test : ℕ
test = ⟦ example ⟧ empty