Church.agda

module Church where

open import Agda.Primitive public using (_⊔_ ; lsuc)


record ⊤ : Set where
  instance
    constructor ∙

infixl 5 _,_
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    π₁ : A
    π₂ : B π₁
open Σ public

infix 2 _×_
_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ A (λ _ → B)


module Native where
  module Bool {A : Set} where
    data Bool : Set where
      true  : Bool
      false : Bool

    if : A → A → Bool → A
    if t f true  = t
    if t f false = f

    meta-if : (P : Bool → Set) → P true → P false → (b : Bool) → P b
    meta-if P t f true  = t
    meta-if P t f false = f

  module Nat {A : Set} where
    data Nat : Set where
      suc  : Nat → Nat
      zero : Nat

    it : (A → A) → A → Nat → A
    it s z (suc n) = s (it s z n)
    it s z zero    = z

    rec : (Nat → A → A) → A → Nat → A
    rec s z (suc n) = s n (rec s z n)
    rec s z zero    = z

    meta-rec : (P : Nat → Set) → ((k : Nat) → P k → P (suc k)) → P zero → (n : Nat) → P n
    meta-rec P s z (suc n) = s n (meta-rec P s z n)
    meta-rec P s z zero    = z


module Shallow where
  module Bool {A : Set} where
    Bool : Set
    Bool = A → A → A

    true : Bool
    true = λ t f → t

    false : Bool
    false = λ t f → f

    if : A → A → Bool → A
    if = λ t f b → b t f

    -- NOTE: Cannot pattern-match on Agda λ-expressions.
    -- meta-if : (P : Bool → Set) → P true → P false → (b : Bool) → P b
    -- meta-if P t f b = {!!}

  module Nat {A : Set} where
    Nat : Set
    Nat = (A → A) → A → A

    -- NOTE: Cannot have recursive type.
    -- Nat′ : Set
    -- Nat′ = (Nat′ → A → A) → A → A

    zero : Nat
    zero = λ f x → x

    suc : Nat → Nat
    suc = λ n f x → f (n f x)

    it : (A → A) → A → Nat → A
    it = λ s z n → n s z

    -- NOTE: Would require recursive type.
    -- rec : (Nat′ → A → A) → A → Nat′ → A
    -- rec = λ s z n → {!!}

    -- NOTE: Cannot pattern-match on Agda λ-expressions.
    -- meta-rec : (P : Nat → Set) → ((k : Nat) → P k → P (suc k)) → P zero → (n : Nat) → P n
    -- meta-rec P s z n = {!!}


module Deep where
  module Contexts (Ty : Set) where
    infixl 5 _,_
    data Cx : Set where
      ∅   : Cx
      _,_ : Cx → Ty → Cx

    infix 3 _∈_
    data _∈_ (A : Ty) : Cx → Set where
      top : ∀ {Γ}   → A ∈ Γ , A
      pop : ∀ {Γ B} → A ∈ Γ → A ∈ Γ , B

    i₀ : ∀ {Γ A} → A ∈ Γ , A
    i₀ = top

    i₁ : ∀ {Γ A B} → A ∈ Γ , A , B
    i₁ = pop top

    i₂ : ∀ {Γ A B C} → A ∈ Γ , A , B , C
    i₂ = pop (pop top)

    infix 3 _⊆_
    data _⊆_ : Cx → Cx → Set where
      done : ∅ ⊆ ∅
      skip : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ ⊆ Γ′ , A
      keep : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ , A ⊆ Γ′ , A

    refl⊆ : ∀ {Γ} → Γ ⊆ Γ
    refl⊆ {∅}     = done
    refl⊆ {Γ , A} = keep refl⊆

    trans⊆ : ∀ {Γ Γ′ Γ″} → Γ ⊆ Γ′ → Γ′ ⊆ Γ″ → Γ ⊆ Γ″
    trans⊆ η        done      = η
    trans⊆ η        (skip η′) = skip (trans⊆ η η′)
    trans⊆ (skip η) (keep η′) = skip (trans⊆ η η′)
    trans⊆ (keep η) (keep η′) = keep (trans⊆ η η′)

    weak⊆ : ∀ {Γ A} → Γ ⊆ Γ , A
    weak⊆ = skip refl⊆

    mono∈ : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → A ∈ Γ → A ∈ Γ′
    mono∈ done     ()
    mono∈ (skip η) i       = pop (mono∈ η i)
    mono∈ (keep η) top     = top
    mono∈ (keep η) (pop i) = pop (mono∈ η i)

  infixr 7 _⇒_
  data Ty : Set where
    _⇒_ : Ty → Ty → Ty
    ⫪   : Ty

  open Contexts (Ty) public

  infix 3 _⊢_
  data _⊢_ (Γ : Cx) : Ty → Set where
    var  : ∀ {A}   → A ∈ Γ → Γ ⊢ A
    lam  : ∀ {A B} → Γ , A ⊢ B → Γ ⊢ A ⇒ B
    app  : ∀ {A B} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
    unit :           Γ ⊢ ⫪

  v₀ : ∀ {Γ A} → Γ , A ⊢ A
  v₀ = var i₀

  v₁ : ∀ {Γ A B} → Γ , A , B ⊢ A
  v₁ = var i₁

  v₂ : ∀ {Γ A B C} → Γ , A , B , C ⊢ A
  v₂ = var i₂

  module NormalForms where
    mutual
      infix 3 _⊢ⁿᶠ_
      data _⊢ⁿᶠ_ (Γ : Cx) : Ty → Set where
        lamⁿᶠ  : ∀ {A B} → Γ , A ⊢ⁿᶠ B → Γ ⊢ⁿᶠ A ⇒ B
        unitⁿᶠ :            Γ ⊢ⁿᶠ ⫪
        neⁿᶠ   : ∀ {A}   → Γ ⊢ⁿᵉ A → Γ ⊢ⁿᶠ A

      infix 3 _⊢ⁿᵉ_
      data _⊢ⁿᵉ_ (Γ : Cx) : Ty → Set where
        varⁿᵉ : ∀ {A}   → A ∈ Γ → Γ ⊢ⁿᵉ A
        appⁿᵉ : ∀ {A B} → Γ ⊢ⁿᵉ A ⇒ B → Γ ⊢ⁿᶠ A → Γ ⊢ⁿᵉ B

    infix 3 _⊢⋆ⁿᶠ_
    _⊢⋆ⁿᶠ_ : Cx → Cx → Set
    Γ ⊢⋆ⁿᶠ ∅     = ⊤
    Γ ⊢⋆ⁿᶠ Ξ , A = Γ ⊢⋆ⁿᶠ Ξ × Γ ⊢ⁿᶠ A

    infix 3 _⊢⋆ⁿᵉ_
    _⊢⋆ⁿᵉ_ : Cx → Cx → Set
    Γ ⊢⋆ⁿᵉ ∅     = ⊤
    Γ ⊢⋆ⁿᵉ Ξ , A = Γ ⊢⋆ⁿᵉ Ξ × Γ ⊢ⁿᵉ A

    mutual
      mono⊢ⁿᶠ : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ ⊢ⁿᶠ A → Γ′ ⊢ⁿᶠ A
      mono⊢ⁿᶠ η (lamⁿᶠ t)    = lamⁿᶠ (mono⊢ⁿᶠ (keep η) t)
      mono⊢ⁿᶠ η unitⁿᶠ       = unitⁿᶠ
      mono⊢ⁿᶠ η (neⁿᶠ t)     = neⁿᶠ (mono⊢ⁿᵉ η t)

      mono⊢ⁿᵉ : ∀ {Γ Γ′ A} → Γ ⊆ Γ′ → Γ ⊢ⁿᵉ A → Γ′ ⊢ⁿᵉ A
      mono⊢ⁿᵉ η (varⁿᵉ i)   = varⁿᵉ (mono∈ η i)
      mono⊢ⁿᵉ η (appⁿᵉ t u) = appⁿᵉ (mono⊢ⁿᵉ η t) (mono⊢ⁿᶠ η u)

    mono⊢⋆ⁿᵉ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ⁿᵉ Ξ → Γ′ ⊢⋆ⁿᵉ Ξ
    mono⊢⋆ⁿᵉ {∅}     η ∙        = ∙
    mono⊢⋆ⁿᵉ {Ξ , A} η (ts , t) = mono⊢⋆ⁿᵉ η ts , mono⊢ⁿᵉ η t

    refl⊢⋆ⁿᵉ : ∀ {Γ} → Γ ⊢⋆ⁿᵉ Γ
    refl⊢⋆ⁿᵉ {∅}     = ∙
    refl⊢⋆ⁿᵉ {Γ , A} = mono⊢⋆ⁿᵉ weak⊆ refl⊢⋆ⁿᵉ , varⁿᵉ top

  module KripkeSemantics where
    record Model : Set₁ where
      field
        World  : Set
        _≤_    : World → World → Set
        refl≤  : ∀ {w} → w ≤ w
        trans≤ : ∀ {w w′ w″} → w ≤ w′ → w′ ≤ w″ → w ≤ w″
    open Model {{…}} public

    infix 3 _⊩_
    _⊩_ : ∀ {{_ : Model}} → World → Ty → Set
    w ⊩ A ⇒ B = ∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B
    w ⊩ ⫪     = ⊤

    infix 3 _⊩⋆_
    _⊩⋆_ : ∀ {{_ : Model}} → World → Cx → Set
    w ⊩⋆ ∅     = ⊤
    w ⊩⋆ Ξ , A = w ⊩⋆ Ξ × w ⊩ A

    mono⊩ : ∀ {{_ : Model}} {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
    mono⊩ {A ⇒ B} ξ s = λ ξ′ a → s (trans≤ ξ ξ′) a
    mono⊩ {⫪}     ξ s = s

    mono⊩⋆ : ∀ {{_ : Model}} {Ξ w w′} → w ≤ w′ → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
    mono⊩⋆ {∅}     ξ ∙       = ∙
    mono⊩⋆ {Ξ , A} ξ (γ , a) = mono⊩⋆ {Ξ} ξ γ , mono⊩ {A} ξ a

    infix 3 _⊨_
    _⊨_ : Cx → Ty → Set₁
    Γ ⊨ A = ∀ {{_ : Model}} {w} → w ⊩⋆ Γ → w ⊩ A

  module Soundness where
    open KripkeSemantics

    eval : ∀ {Γ A} → Γ ⊢ A → Γ ⊨ A
    eval (var top)     γ = π₂ γ
    eval (var (pop i)) γ = eval (var i) (π₁ γ)
    eval (lam t)       γ = λ ξ a → eval t (mono⊩⋆ ξ γ , a)
    eval (app t u)     γ = (eval t γ refl≤) (eval u γ)
    eval unit          γ = ∙

  module Completeness where
    open KripkeSemantics
    open NormalForms public

    instance
      canon : Model
      canon = record
        { World  = Cx
        ; _≤_    = _⊆_
        ; refl≤  = refl⊆
        ; trans≤ = trans⊆
        }

    mutual
      reflectᶜ : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ⊩ A
      reflectᶜ {A ⇒ B} t = λ η a → reflectᶜ (appⁿᵉ (mono⊢ⁿᵉ η t) (reifyᶜ a))
      reflectᶜ {⫪}     t = ∙

      reifyᶜ : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ⁿᶠ A
      reifyᶜ {A ⇒ B} s = lamⁿᶠ (reifyᶜ (s weak⊆ (reflectᶜ {A} (varⁿᵉ top))))
      reifyᶜ {⫪}     s = unitⁿᶠ

    reflectᶜ⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ⁿᵉ Ξ → Γ ⊩⋆ Ξ
    reflectᶜ⋆ {∅}     ∙        = ∙
    reflectᶜ⋆ {Ξ , A} (ts , t) = reflectᶜ⋆ ts , reflectᶜ t

    reifyᶜ⋆ : ∀ {Ξ Γ} → Γ ⊩⋆ Ξ → Γ ⊢⋆ⁿᶠ Ξ
    reifyᶜ⋆ {∅}     ∙        = ∙
    reifyᶜ⋆ {Ξ , A} (ts , t) = reifyᶜ⋆ ts , reifyᶜ t

    refl⊩⋆ : ∀ {Γ} → Γ ⊩⋆ Γ
    refl⊩⋆ = reflectᶜ⋆ refl⊢⋆ⁿᵉ

    quot : ∀ {Γ A} → Γ ⊨ A → Γ ⊢ⁿᶠ A
    quot s = reifyᶜ (s refl⊩⋆)

  module NormalisationByEvaluation where
    open Soundness
    open Completeness

    norm : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ⁿᶠ A
    norm t = quot (eval t)

  module Bool {A : Ty} where
    Bool : Ty
    Bool = A ⇒ A ⇒ A

    true : ∀ {Γ} → Γ ⊢ Bool
    true = lam (lam v₁)

    false : ∀ {Γ} → Γ ⊢ Bool
    false = lam (lam v₀)

    if : ∀ {Γ} → Γ ⊢ A ⇒ A ⇒ Bool ⇒ A
    if = lam (lam (lam (app (app v₀ v₂) v₁)))

    -- NOTE: Too meta.
    -- meta-if : (P : ∅ ⊢ Bool → Set) → P true → P false → (b : ∅ ⊢ Bool) → P b
    -- meta-if P t f b = {!!}

  module Nat {A : Ty} where
    Nat : Ty
    Nat = (A ⇒ A) ⇒ A ⇒ A

    -- NOTE: Cannot have recursive type.
    -- Nat′ : Ty
    -- Nat′ = (Nat′ ⇒ A ⇒ A) ⇒ A ⇒ A

    zero : ∀ {Γ} → Γ ⊢ Nat
    zero = lam (lam v₀)

    suc : ∀ {Γ} → Γ ⊢ Nat ⇒ Nat
    suc = lam (lam (lam (app v₁ (app (app v₂ v₁) v₀))))

    it : ∀ {Γ} → Γ ⊢ (A ⇒ A) ⇒ A ⇒ Nat ⇒ A
    it = lam (lam (lam (app (app v₀ v₂) v₁)))

    -- NOTE: Would require recursive type.
    -- rec : ∀ {Γ} → Γ ⊢ (Nat′ ⇒ A ⇒ A) ⇒ A ⇒ Nat′ ⇒ A
    -- rec = lam (lam (lam {!!}))

    -- NOTE: Too meta.
    -- meta-rec : (P : ∅ ⊢ Nat → Set) → ((k : ∅ ⊢ Nat) → P k → P (app suc k)) → P zero → (n : ∅ ⊢ Nat) → P n
    -- meta-rec P s z n = {!!}