Simply typed lambda calculus with extensions

SimplyTypedLambdaCalculus.agda

module SimplyTypedLambdaCalculus where

  open import Data.Bool
  open import Data.Nat hiding (erase)
  import Data.Unit
  open import Data.Maybe
  open import Data.Product
  open import Data.Sum
  open import Relation.Binary.PropositionalEquality hiding ([_])
  open import Relation.Nullary
  open import Relation.Nullary.Decidable
  import Data.String
  open import Data.Nat.Show
  open import Data.List hiding ([_])
  open import Data.Empty
  open import Function

  data Type : Set where
    `Nat  : Type
    `Bool : Type
    `Unit : Type
    `_⇒_  : Type → Type → Type
    `_×_  : Type → Type → Type
    `_⊎_  : Type → Type → Type

  -- Embedding types
  -- Semantics of the syntax
  [_]ᵗ : Type → Set
  [ `Nat ]ᵗ = ℕ
  [ `Bool ]ᵗ = Bool
  [ `Unit ]ᵗ = Data.Unit.⊤
  [ ` A ⇒ B ]ᵗ = [ A ]ᵗ → [ B ]ᵗ
  [ ` A × B ]ᵗ = [ A ]ᵗ × [ B ]ᵗ
  [ ` A ⊎ B ]ᵗ = [ A ]ᵗ ⊎ [ B ]ᵗ

  Id : Set
  Id = Data.String.String

  Context : Set
  Context = List (Id × Type)

  data _∈_ : Id → Context → Set where
    here  : ∀ {x τ Γ} → x ∈ ((x , τ) ∷ Γ)
    there : ∀ {x y τ Γ} → x ∈ Γ → x ∈ ((y , τ) ∷ Γ)

  lookupType : (x : Id) (Γ : Context) → x ∈ Γ → Type
  lookupType x [] ()
  lookupType x ((_ , τ) ∷ Γ) here = τ
  lookupType x (_ ∷ Γ) (there pf) = lookupType x Γ pf

  contradiction : ∀ {ℓ} {A : Set ℓ} → A → (¬ A) → ⊥
  contradiction x y = y x

  skipOne : ∀ {Γ x y τ} → ¬ (x ≡ y) → x ∈ ((y , τ) ∷ Γ) → x ∈ Γ
  skipOne neq here = ⊥-elim (neq refl)
  skipOne neq (there i) = i

  lookup : (x : Id) (Γ : Context) → Dec (x ∈ Γ)
  lookup x [] = no (λ ())
  lookup x ((y , τ) ∷ Γ) with x Data.String.≟ y
  lookup x ((.x , τ) ∷ Γ) | yes refl = yes here
  lookup x ((y , τ) ∷ Γ) | no q with lookup x Γ
  ... | yes p = yes (there p)
  ... | no q' = no ((λ i → contradiction i q') ∘ skipOne q)

  -- Terms that have to type check by definition.
  data _⊢_ : Context → Type → Set where
    `tt : ∀ {Γ} → Γ ⊢ `Unit
    -- Boolean terms
    `true : ∀ {Γ} → Γ ⊢ `Bool
    `false : ∀ {Γ} → Γ ⊢ `Bool
    `_∧_ : ∀ {Γ} → Γ ⊢ `Bool → Γ ⊢ `Bool → Γ ⊢ `Bool
    `_∨_ : ∀ {Γ} → Γ ⊢ `Bool →  Γ ⊢ `Bool → Γ ⊢ `Bool
    `¬_ : ∀ {Γ} → Γ ⊢ `Bool →  Γ ⊢ `Bool
    `if_`then_`else_ : ∀ {Γ τ} → Γ ⊢ `Bool → Γ ⊢ τ → Γ ⊢ τ → Γ ⊢ τ
    -- ℕ terms
    `n_ : ∀ {Γ} → ℕ → Γ ⊢ `Nat
    `_≤_ : ∀ {Γ} → Γ ⊢ `Nat → Γ ⊢ `Nat →  Γ ⊢ `Bool
    `_+_ : ∀ {Γ} → Γ ⊢ `Nat → Γ ⊢ `Nat → Γ ⊢ `Nat
    `_*_ : ∀ {Γ} → Γ ⊢ `Nat →  Γ ⊢ `Nat → Γ ⊢ `Nat
    -- Abstraction & context terms
    `v : ∀ {Γ} → (x : Id) → (i : x ∈ Γ) → Γ ⊢ lookupType x Γ i
    `_·_ : ∀ {Γ τ σ} → Γ ⊢ (` τ ⇒ σ) → Γ ⊢ τ → Γ ⊢ σ
    `λ_`:_⇒_ : ∀ {Γ τ} → (x : Id) → (σ : Type) → ((x , σ) ∷ Γ) ⊢ τ → Γ ⊢ (` σ ⇒ τ)
    `let_`=_`in_ : ∀ {Γ τ σ} → (x : Id) → Γ ⊢ τ → ((x , τ) ∷ Γ) ⊢ σ → Γ ⊢ σ
    -- Product and sum terms
    `_,_ : ∀ {Γ τ σ} → Γ ⊢ τ →  Γ ⊢ σ →  Γ ⊢ (` τ × σ)
    `fst : ∀ {Γ τ σ} → Γ ⊢ (` τ × σ) → Γ ⊢ τ
    `snd : ∀ {Γ τ σ} → Γ ⊢ (` τ × σ) → Γ ⊢ σ
    `inl_`as_ : ∀ {Γ τ} → Γ ⊢ τ → (σ : Type) → Γ ⊢ (` τ ⊎ σ)
    `inr_`as_ : ∀ {Γ σ} → Γ ⊢ σ → (τ : Type) → Γ ⊢ (` τ ⊎ σ)
    `case_`of_||_ : ∀ {Γ τ σ υ} → Γ ⊢ (` τ ⊎ σ) → Γ ⊢ (` τ ⇒ υ) → Γ ⊢ (` σ ⇒ υ) → Γ ⊢ υ

  Closed : Type → Set
  Closed = _⊢_ []

  {- Defining an abstract syntax tree.
     Unlike the terms _⊢_, these can fail type checking.
  -}
  data Expr : Set where
    EUnit ETrue EFalse : Expr
    EVar : Id → Expr
    ENat : ℕ → Expr
    EAnd EOr EPlus ETimes ELte EApp EPair : Expr → Expr → Expr
    ENot EFst ESnd : Expr → Expr
    ECond ECase : Expr → Expr → Expr → Expr
    ELet : Id → Expr → Expr → Expr
    ELam : Id → Type → Expr → Expr
    EInl EInr : Expr → Type → Expr

  -- Type erasure. Get a syntactical expr from a type checked term.
  erase : ∀ {τ Γ} → Γ ⊢ τ → Expr
  erase `tt = EUnit
  erase `true = ETrue
  erase `false = EFalse
  erase (` x ∧ y) = EAnd (erase x) (erase y)
  erase (` x ∨ y) = EOr (erase x) (erase y)
  erase (`¬ x) = ENot (erase x)
  erase (`if c `then x `else y) = ECond (erase c) (erase x) (erase y)
  erase (`n x) = ENat x
  erase (` x ≤ y) = ELte (erase x) (erase y)
  erase (` x + y) = EPlus (erase x) (erase y)
  erase (` x * y) = ETimes (erase x) (erase y)
  erase (`v id i) = EVar id
  erase (` x · y) = EApp (erase x) (erase y)
  erase (`λ id `: σ ⇒ τ) = ELam id σ (erase τ)
  erase (`let id `= x `in y) = ELet id (erase x) (erase y)
  erase (` x , y) = EPair (erase x) (erase y)
  erase (`fst p) = EFst (erase p)
  erase (`snd p) = ESnd (erase p)
  erase (`inl x `as σ) = EInl (erase x) σ
  erase (`inr x `as τ) = EInr (erase x) τ
  erase (`case x `of f || g) = ECase (erase x) (erase f) (erase g)

  ≡⇒ : ∀ {σ σ′ τ τ′} → ` σ ⇒ τ ≡ ` σ′ ⇒ τ′ → (σ ≡ σ′) × (τ ≡ τ′)
  ≡⇒ refl = refl , refl
  ≡× : ∀ {σ σ′ τ τ′} → ` σ × τ ≡ ` σ′ × τ′ → (σ ≡ σ′) × (τ ≡ τ′)
  ≡× refl = refl , refl
  ≡⊎ : ∀ {σ σ′ τ τ′} → ` σ ⊎ τ ≡ ` σ′ ⊎ τ′ → (σ ≡ σ′) × (τ ≡ τ′)
  ≡⊎ refl = refl , refl

  mutual
    relDec : (x y x' y' : Type) → (R : Type → Type → Type)
            → (∀ {σ σ′ τ τ′} → R σ τ ≡ R σ′ τ′ → (σ ≡ σ′) × (τ ≡ τ′))
            → Dec ((R x y) ≡ (R x' y'))
    relDec x y x' y' R ≡R with x dec x' | y dec y'
    relDec x y .x .y R ≡R | yes refl | yes refl = yes refl
    relDec x y x' y' R ≡R | no ¬p | _ = no (¬p ∘ proj₁ ∘ ≡R)
    relDec x y x' y' R ≡R | _ | no ¬q = no (¬q ∘ proj₂ ∘ ≡R)

    _dec_ : (τ σ : Type) → Dec (τ ≡ σ)
    `Nat dec `Nat = yes refl
    `Nat dec `Bool = no (λ ())
    `Nat dec `Unit = no (λ ())
    `Nat dec (` _ ⇒ _) = no (λ ())
    `Nat dec (` _ × _) = no (λ ())
    `Nat dec (` _ ⊎ _) = no (λ ())
    `Bool dec `Nat =  no (λ ())
    `Bool dec `Bool = yes refl
    `Bool dec `Unit = no (λ ())
    `Bool dec (` _ ⇒ _) = no (λ ())
    `Bool dec (` _ × _) = no (λ ())
    `Bool dec (` _ ⊎ _) = no (λ ())
    `Unit dec `Nat = no (λ ())
    `Unit dec `Bool = no (λ ())
    `Unit dec `Unit = yes refl
    `Unit dec (` _ ⇒ _) = no (λ ())
    `Unit dec (` _ × _) = no (λ ())
    `Unit dec (` _ ⊎ _) = no (λ ())
    (` _ ⇒ _) dec `Nat = no (λ ())
    (` _ ⇒ _) dec `Bool = no (λ ())
    (` _ ⇒ _) dec `Unit = no (λ ())
    (` σ ⇒ τ) dec (` σ' ⇒ τ') = relDec σ τ σ' τ' `_⇒_ ≡⇒
    (` _ ⇒ _) dec (` _ × _) = no (λ ())
    (` _ ⇒ _) dec (` _ ⊎ _) = no (λ ())
    (` _ × _) dec `Nat = no (λ ())
    (` _ × _) dec `Bool = no (λ ())
    (` _ × _) dec `Unit = no (λ ())
    (` _ × _) dec (` _ ⇒ _) = no (λ ())
    (` σ × τ) dec (` σ' × τ') = relDec σ τ σ' τ' `_×_ ≡×
    (` _ × _) dec (` _ ⊎ _) = no (λ ())
    (` _ ⊎ _) dec `Nat = no (λ ())
    (` _ ⊎ _) dec `Bool = no (λ ())
    (` _ ⊎ _) dec `Unit = no (λ ())
    (` _ ⊎ _) dec (` _ ⇒ _) = no (λ ())
    (` _ ⊎ _) dec (` _ × _) = no (λ ())
    (` σ ⊎ τ) dec (` σ' ⊎ τ') = relDec σ τ σ' τ' `_⊎_ ≡⊎

  data Check (Γ : Context) : Expr → Set where
    well : (τ : Type) (t : Γ ⊢ τ) → Check Γ (erase t)
    ill  : {e : Expr} → Check Γ e

  check : (Γ : Context) (e : Expr) → Check Γ e
  check Γ EUnit = well `Unit `tt
  check Γ ETrue = well `Bool `true
  check Γ EFalse = well `Bool `false
  check Γ (EVar id) with lookup id Γ
  check _ (EVar id) | yes p = well _ (`v id p)
  ... | no q = ill
  check Γ (ENat x) = well `Nat (`n x)
  check Γ (EAnd x y) with check Γ x | check Γ y
  check Γ (EAnd .(erase t) .(erase u)) | well `Bool t | well `Bool u = well `Bool (` t ∧ u)
  check Γ (EAnd _ _) | _ | _ = ill
  check Γ (EOr x y) with check Γ x | check Γ y
  check Γ (EOr .(erase t) .(erase u)) | well `Bool t | well `Bool u = well `Bool (` t ∨ u)
  check Γ (EOr _ _) | _ | _ = ill
  check Γ (EPlus x y) with check Γ x | check Γ y
  check Γ (EPlus .(erase t) .(erase u)) | well `Nat t | well `Nat u = well `Nat (` t + u)
  check Γ (EPlus _ _) | _ | _ = ill
  check Γ (ETimes x y) with check Γ x | check Γ y
  check Γ (ETimes .(erase t) .(erase u)) | well `Nat t | well `Nat u = well `Nat (` t * u)
  check Γ (ETimes _ _) | _ | _ = ill
  check Γ (ELte x y) with check Γ x | check Γ y
  check Γ (ELte .(erase t) .(erase u)) | well `Nat t | well `Nat u = well `Bool (` t ≤ u)
  check Γ (ELte _ _) | _ | _ = ill
  check Γ (EApp x y)  with check Γ x | check Γ y
  check Γ (EApp .(erase t) .(erase u)) | well (` σ ⇒ τ) t | well σ' u with σ dec σ'
  check Γ (EApp .(erase t) .(erase u)) | well (` σ' ⇒ τ) t | well .σ' u | yes refl = well τ (` t · u)
  ... | no _ = ill
  check Γ (EApp x y) | _ | _ = ill
  check Γ (EPair x y) with check Γ x | check Γ y
  check Γ (EPair .(erase t) .(erase u)) | well τ t | well σ u = well (` τ × σ) (` t , u)
  check Γ (EPair x y) | _ | _ = ill
  check Γ (ENot e) with check Γ e
  check Γ (ENot .(erase t)) | well `Bool t = well `Bool (`¬ t)
  check Γ (ENot e) | _ = ill
  check Γ (EFst e) with check Γ e
  check Γ (EFst .(erase t)) | well (` τ × σ) t = well τ (`fst t)
  check Γ (EFst e) | _ = ill
  check Γ (ESnd e) with check Γ e
  check Γ (ESnd .(erase t)) | well (` τ × σ) t = well σ (`snd t)
  check Γ (ESnd e) | _ = ill
  check Γ (EInl e σ) with check Γ e
  check Γ (EInl .(erase t) σ) | well τ t = well (` τ ⊎ σ) (`inl t `as σ)
  check Γ (EInl e σ) | ill = ill
  check Γ (EInr e τ) with check Γ e
  check Γ (EInr .(erase t) τ) | well σ t = well (` τ ⊎ σ) (`inr t `as τ)
  check Γ (EInr _ _) | ill = ill
  check Γ (ECond c x y) with check Γ c | check Γ x | check Γ y
  check Γ (ECond .(erase t) .(erase u) .(erase v)) | well `Bool t | well τ u | well σ v with τ dec σ
  check Γ (ECond .(erase t) .(erase u) .(erase v)) | well `Bool t | well σ u | well .σ v | yes refl = well σ (`if t `then u `else v)
  ... | no _ = ill
  check Γ (ECond c x y) | _ | _ | _ = ill
  check Γ (ECase c x y) with check Γ c | check Γ x | check Γ y
  check Γ (ECase .(erase t) .(erase u) .(erase v)) | well (` τ ⊎ σ) t | well (` τ' ⇒ υ) u | well (` σ' ⇒ υ') v with τ dec τ' | σ dec σ' | υ dec υ'
  check Γ (ECase .(erase t) .(erase u) .(erase v)) | well (` τ' ⊎ σ') t | well (` .τ' ⇒ υ') u | well (` .σ' ⇒ .υ') v | yes refl | yes refl | yes refl =
    well υ' (`case t `of u || v)
  ... | _ | _ | _ = ill
  check Γ (ECase c x y) | _ | _ | _ = ill
  check Γ (ELet id x y) with check Γ x
  check Γ (ELet id .(erase t) y) | well τ t with check ((id , τ) ∷ Γ) y
  check Γ (ELet id .(erase t) .(erase u)) | well τ t | well σ u = well σ (`let id `= t `in u)
  check Γ (ELet id .(erase t) y) | well τ t | ill = ill
  check Γ (ELet id x y) | ill = ill
  check Γ (ELam id σ y) with check ((id , σ) ∷ Γ) y
  check Γ (ELam id σ .(erase t)) | well τ t = well (` σ ⇒ τ) (`λ id `: σ ⇒ t )
  check Γ (ELam id σ y) | ill = ill

  -- Interpretation

  data Env : Context → Set₁ where
    E  : Env  []
    C  : ∀ {x τ Γ} → [ τ ]ᵗ → Env Γ → Env ((x , τ) ∷ Γ)

  lookupEnv : ∀ {x Γ} → Env Γ → (mem : x ∈ Γ) → [ lookupType x Γ mem ]ᵗ
  lookupEnv E ()
  lookupEnv (C τᵗ env) here =  τᵗ
  lookupEnv (C _ env) (there mem) = lookupEnv env mem

  -- Interpretation under a given context.
  interpret : ∀ {τ Γ} → Env Γ → Γ ⊢ τ → [ τ ]ᵗ
  interpret env `tt = Data.Unit.tt
  interpret env `true = true
  interpret env `false = false
  interpret env (` x ∧ y) = (interpret env x) ∧ (interpret env y)
  interpret env (` x ∨ y) = (interpret env x) ∨ (interpret env y)
  interpret env (`¬ x) = not (interpret env x)
  interpret env (`if c `then x `else y) =
    if (interpret env c) then (interpret env x) else (interpret env y)
  interpret env (`n x) = x
  interpret env (` x ≤ y) =
    ⌊ ( interpret env x )  ≤? ( interpret env y )  ⌋
  interpret env (` x + y) = (interpret env x) + (interpret env y)
  interpret env (` x * y) = (interpret env x) * (interpret env y)
  interpret env (`v x i) = lookupEnv env i
  interpret env (` f · x) = (interpret env f) (interpret env x)
  interpret env (`λ _ `: σ ⇒ τ) = λ (x : [ σ ]ᵗ) → interpret (C x env) τ
  interpret env (`let id `= x `in y) = let val = interpret env x in interpret (C val env) y
  interpret env (` x , y) = interpret env x , interpret env y
  interpret env (`fst p) = proj₁ (interpret env p)
  interpret env (`snd p) = proj₂ (interpret env p)
  interpret env (`inl x `as _) = inj₁ (interpret env x)
  interpret env (`inr y `as _) = inj₂ (interpret env y)
  interpret env (`case x `of f || g) =
    [  interpret env f ,  interpret env g ]′ (interpret env x)

  -- Interpretation of closed terms.
  [_] : ∀ {τ} → Closed τ → [ τ ]ᵗ
  [ x ] = interpret E x

  2+2 : Closed `Nat
  2+2 = ` (`λ "x" `: `Nat ⇒ (` (`v "x" here) + (`v "x" here))) · `n 2

  2+2≡4 : [ 2+2 ] ≡ 4
  2+2≡4 = refl

  expr+double : Expr
  expr+double = ELam "x" `Nat (EPlus (EVar "x") (EVar "x"))

  term+double : Closed ( ` `Nat ⇒ `Nat)
  term+double = `λ "x" `: `Nat ⇒ (` (`v "x" here) + (`v "x" here))

  check+double : check [] expr+double ≡ well (` `Nat ⇒ `Nat) term+double
  check+double = refl