Simply Typed Lambda Calculus

STLC.agda

module _ where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat
{-# BUILTIN NATURAL Nat #-}

_+_ : (n m : Nat) -> Nat
zero + m = m
suc n + m = suc (n + m)

data Vec (A : Set) : Nat -> Set where
  nil : Vec A zero
  _::_ : A -> {n : Nat} -> Vec A n -> Vec A (suc n)

infixr 5 _::_

data Fin : Nat -> Set where
  zero : {n : Nat} -> Fin (suc n)
  suc : {n : Nat} -> Fin n -> Fin (suc n)

toNat : {n : Nat} -> Fin n -> Nat
toNat zero = zero
toNat (suc n) = suc (toNat n)

_!_ : {A : Set} -> {n : Nat} -> Vec A n -> Fin n -> A
(x :: xs) ! zero = x
(x :: xs) ! suc i = xs ! i

data Syntax : Set where
  var : Nat -> Syntax
  lam : Syntax -> Syntax
  _$_ : (f x : Syntax) -> Syntax
  nat : Nat -> Syntax
  _⊕_ : (n m : Syntax) -> Syntax

data Type : Set where
  nat : Type
  _=>_ : (σ τ : Type) -> Type

data Term {n : Nat} (Ctx : Vec Type n) : Type -> Set where
  var : (n' : Fin n) -> Term Ctx (Ctx ! n')
  lam : (σ τ : Type) -> Term (σ :: Ctx) τ -> Term Ctx (σ => τ)
  _$_ : (σ τ : Type) -> Term Ctx (σ => τ) -> Term Ctx σ -> Term Ctx τ
  nat : Nat -> Term Ctx nat
  _⊕_ : (n m : Term Ctx nat) -> Term Ctx nat

erase : {n : Nat} (Ctx : Vec Type n) (σ : Type) -> Term Ctx σ -> Syntax
erase Ctx .(Ctx ! n') (var n') = var (toNat n')
erase Ctx .(σ => τ) (lam σ τ x) = lam (erase (σ :: Ctx) τ x)
erase Ctx σ ((τ $ .σ) f x) = erase Ctx (τ => σ) f $ erase Ctx τ x
erase Ctx .nat (nat x) = nat x
erase Ctx .nat (n ⊕ m) = erase Ctx nat n ⊕ erase Ctx nat m