module Semantics.SystemT where open import IType.Nat open import IFam.Fin open import IFam.Vector renaming (_::_ to cons) data Ty : Set where NF : Ty _⇒_ : Ty → Ty → Ty Ctx : Nat → Set Ctx n = Vect Ty n infixr 60 _⇒_ -- the set of n-place functions following Aczel data F : Nat → Set where var : {n : Nat} → Fin n → F n _#_ : {n : Nat} → F n → F n → F n -- application lam : {n : Nat} → F (succ n) → F n zeroF : {n : Nat} → F n succF : {n : Nat} → F n recF : {n : Nat} → F n -- syntactic typing data _⊢_∈_ : {n : Nat} → Ctx n → F n → Ty → Set where var-ty : {n : Nat} → {Γ : Ctx n} → {i : Fin n} → Γ ⊢ var i ∈ lookup i Γ app-ty : {n : Nat} → {Γ : Ctx n} → {A B : Ty} → {c a : F n} → Γ ⊢ c ∈ A ⇒ B → Γ ⊢ a ∈ A → Γ ⊢ c # a ∈ B lam-ty : {n : Nat} → {Γ : Ctx n} → {A B : Ty} → {b : F (succ n)} → {a : F n} → cons A Γ ⊢ b ∈ B → Γ ⊢ lam b ∈ A ⇒ B -- etc for types of zeroF, succF, recF infixl 50 _#_ -- Canonical forms data Val : Set where lamV : F 1 → Val zeroV : Val succV : F 0 → Val -- we leave substitution as a postulate. Exercise: define it! postulate _[_] : F 1 → F 0 → F 0 -- computation rules (big step semantics, natural semantics) data _=>_ : F 0 → Val → Set where β : {c a : F 0} → {b : F 1} → {v : Val} → c => lamV b → b [ a ] => v → c # a => v lamVal : {b : F 1} → lam b => lamV b zeroVal : zeroF => zeroV succVal : {a : F 0} → succF # a => succV a reczeroVal : {n d e : F 0} → {v : Val} → n => zeroV → d => v → recF # d # e # n => v recsuccVal : {m n d e : F 0} → {v : Val} → n => succV m → e # m # (recF # d # e # m) => v → recF # d # e # n => v -- Semantic natural numbers data isN : F 0 → Set where zeroN : {a : F 0} → a => zeroV → isN a succN : {a b : F 0} → a => succV b → isN b → isN a -- Semantic typing of closed terms _::_ : F 0 → Ty → Set c :: NF = isN c c :: A ⇒ B = (a : F 0) → a :: A → c # a :: B -- Typing open terms -- unncessary because can be reduced to typing functions Env : Nat → Set Env n = Vect (F 0) n data _fits_ : {n : Nat} → Env n → Ctx n → Set where nilfits : [] fits [] consfits : {n : Nat} → {a : F 0} → {A : Ty} → {ρ : Env n} → {Γ : Ctx n} → a :: A → ρ fits Γ → cons a ρ fits cons A Γ postulate inst : {n : Nat} → F n → Env n → F 0 opentyping : {n : Nat} → Ctx n → F n → Ty → Set opentyping {n} Γ a A = (ρ : Env n) → ρ fits Γ → inst a ρ :: A _⊢_::_ : {n : Nat} → Ctx n → F n → Ty → Set Γ ⊢ a :: A = opentyping Γ a A -- syntactic typing implies semantic typing -- soundness : {n : Nat} → {Γ : Ctx n} → {a : F n} → {A : Ty} -- → Γ ⊢ a ∈ A -- → Γ ⊢ a :: A