Programming Language Foundations in Agda: Lambda

Lambda.agda

module Lambda where

open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product using (_×_; _,_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Data.List using (List; _∷_; [])

-- https://gist.github.com/pedrominicz/bce9bcfc44f55c04ee5e0b6d903f5809
open import Isomorphism using (_≃_; _≲_)

Id : Set
Id = String

infix  5 ƛ_⇒_
infix  5 μ_⇒_
infixl 7 _·_
infix  8 `suc_
infix  9 `_

data Term : Set where
    `_                      : Id → Term
    ƛ_⇒_                    : Id → Term → Term
    _·_                     : Term → Term → Term
    `zero                   : Term
    `suc_                   : Term → Term
    case_[zero⇒_|suc_⇒_]    : Term → Term → Id → Term → Term
    μ_⇒_                    : Id → Term → Term

one : Term
one = `suc `zero

two : Term
two = `suc `suc `zero

plus : Term
plus =
    μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
        case `"m"
            [zero⇒ `"n"
            |suc "m" ⇒ `suc (`"+" · `"m" · `"n")]

sucᶜ : Term
sucᶜ = ƛ "n" ⇒ `suc (`"n")

twoᶜ : Term
twoᶜ = ƛ "s" ⇒ ƛ "z" ⇒ `"s" · (`"s" · `"z")

plusᶜ : Term
plusᶜ =
    ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
        `"m" · `"s" · (`"n" · `"s" · `"z")

mul : Term
mul =
    μ "*" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
        case `"m"
            [zero⇒ `zero
            |suc "m" ⇒ plus · `"n" · (`"*" · `"m" · `"n")]

mulᶜ : Term
mulᶜ =
    ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
        `"m" · (`"n" · `"s") · `"z"

ƛ'_⇒_ : Term → Term → Term
ƛ' (` x) ⇒ N = ƛ x ⇒ N
ƛ' _ ⇒ _     = ⊥-elim impossible
    where
    postulate
        impossible : ⊥

case'_[zero⇒_|suc_⇒_] : Term → Term → Term → Term → Term
case' L [zero⇒ M |suc (` x) ⇒ N ] = case L [zero⇒ M |suc x ⇒ N ]
case' _ [zero⇒ _ |suc _ ⇒ _ ]     = ⊥-elim impossible
    where
    postulate
        impossible : ⊥

μ'_⇒_ : Term → Term → Term
μ' (` x) ⇒ N = μ x ⇒ N
μ' _ ⇒ _     = ⊥-elim impossible
    where
    postulate
        impossible : ⊥

plus' : Term
plus' =
    μ' + ⇒ ƛ' m ⇒ ƛ' n ⇒
        case' m
            [zero⇒ n
            |suc m ⇒ `suc (+ · m · n)]
    where
    + = `"+"
    m = `"m"
    n = `"n"

mul' : Term
mul' =
    μ' * ⇒ ƛ' m ⇒ ƛ' n ⇒
        case' m
            [zero⇒ `zero
            |suc m ⇒ plus' · n · (* · m · n)]
    where
    * = `"*"
    m = `"m"
    n = `"n"

data Value : Term → Set where
    V-ƛ    : ∀ {x : Id} {N : Term} → Value (ƛ x ⇒ N)
    V-zero : Value `zero
    V-suc  : ∀ {V : Term} → Value V → Value (`suc V)

infix 9 _[_:=_]

_[_:=_] : Term → Id → Term → Term
(` x) [ y := V ] with x ≟ y
...                 | yes _ = V
...                 | no _  = ` x
(ƛ x ⇒ N) [ y := V ] with x ≟ y
...                     | yes _ = ƛ x ⇒ N
...                     | no _  = ƛ x ⇒ N [ y := V ]
(L · M) [ y := V ]  = L [ y := V ] · M [ y := V ]
`zero [ y := V ]    = `zero
(`suc M) [ y := V ] = `suc M [ y := V ]
case L [zero⇒ M |suc x ⇒ N ] [ y := V ]
    with x ≟ y
...    | yes _ = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N ]
...    | no _  = case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N [ y := V ] ]
(μ x ⇒ N) [ y := V ] with x ≟ y
...                     | yes _ = μ x ⇒ N
...                     | no _  = μ x ⇒ N [ y := V ]

[:=]'-helper : Id → Id → Term → Term → Term
[:=]'-helper x y N V with x ≟ y
...                     | yes _ = N [ y := V ]
...                     | no _  = N

_[_:=_]' : Term → Id → Term → Term
(` x) [ y := V ]' with x ≟ y
...                  | yes _ = V
...                  | no _  = ` x
(ƛ x ⇒ N) [ y := V ]' = ƛ x ⇒ [:=]'-helper x y N V
(L · M) [ y := V ]'   = L [ y := V ]' · M [ y := V ]'
`zero [ y := V ]'     = `zero
(`suc M) [ y := V ]'  = `suc M [ y := V ]'
case L [zero⇒ M |suc x ⇒ N ] [ y := V ]' =
    case L [ y := V ]' [zero⇒ M [ y := V ]' |suc x ⇒ [:=]'-helper x y N V ]
(μ x ⇒ N) [ y := V ]' = μ x ⇒ [:=]'-helper x y N V

infix 4 _—→_

data _—→_ : Term → Term → Set where
    ξ-·₁ : ∀ {L L' M : Term}
        → L —→ L'
        -----------------
        → L · M —→ L' · M

    ξ-·₂ : ∀ {V M M' : Term}
        → Value V
        → M —→ M'
        -----------------
        → V · M —→ V · M'

    β-ƛ : ∀ {x : Id} {N V : Term}
        → Value V
        -------------------------------
        → (ƛ x ⇒ N) · V —→ N [ x := V ]

    ξ-suc : ∀ {M M' : Term}
        → M —→ M'
        -------------------
        → `suc M —→ `suc M'

    ξ-case : ∀ {x : Id} {L L' M N : Term}
        → L —→ L'
        ---------------------------------------------------------------
        → case L [zero⇒ M |suc x ⇒ N ] —→ case L' [zero⇒ M |suc x ⇒ N ]

    β-zero : ∀ {x : Id} {M N : Term}
        ---------------------------------------
        → case `zero [zero⇒ M |suc x ⇒ N ] —→ M

    β-suc : ∀ {x : Id} {V M N : Term}
        → Value V
        ---------------------------------------------------
        → case `suc V [zero⇒ M |suc x ⇒ N ] —→ N [ x := V ]

    β-μ : ∀ {x : Id} {M : Term}
        -------------------------------
        → μ x ⇒ M —→ M [ x := μ x ⇒ M ]

infix  2 _—→→_
infix  1 begin_
infixr 2 _—→⟨_⟩_
infix  3 _∎

data _—→→_ : Term → Term → Set where
    _∎ : ∀ (M : Term)
        ---------
        → M —→→ M

    _—→⟨_⟩_ : ∀ (L : Term) {M N : Term}
        → L —→ M
        → M —→→ N
        ---------
        → L —→→ N

begin_ : ∀ {M N : Term}
    → M —→→ N
    ---------
    → M —→→ N
begin M—→→N = M—→→N

data _—→→'_ : Term → Term → Set where
    step' : ∀ {M N : Term}
        → M —→ N
        ----------
        → M —→→' N

    refl' : ∀ {M : Term}
        ----------
        → M —→→' M

    trans' : ∀ {L M N : Term}
        → L —→→' M
        → M —→→' N
        ----------
        → L —→→' N

—→→≲—→→' : ∀ {M N : Term} → M —→→ N ≲ M —→→' N
—→→≲—→→' = record
    { to      = to
    ; from    = from
    ; from∘to = from∘to
    }
    where
    to : ∀ {M N : Term} → M —→→ N → M —→→' N
    to (M ∎)                = refl'
    to (L —→⟨ L—→M ⟩ M—→→N) = trans' (step' L—→M) (to M—→→N)

    trans : ∀ {L M N : Term} → L —→→ M → M —→→ N → L —→→ N
    trans (L ∎)            M—→→N = M—→→N
    trans (L —→⟨ L—→M ⟩ M) M—→→N = L —→⟨ L—→M ⟩ (trans M M—→→N)

    from : ∀ {M N : Term} → M —→→' N → M —→→ N
    from (step' {M} {N} M—→N)   = M —→⟨ M—→N ⟩ N ∎
    from (refl' {M})            = M ∎
    from (trans' L—→→'M M—→→'N) = trans (from L—→→'M) (from M—→→'N)

    from∘to : ∀ {M N : Term} (x : M —→→ N) → from (to x) ≡ x
    from∘to (M ∎)                              = refl
    from∘to (M —→⟨ M—→N ⟩ N) rewrite from∘to N = refl

_ : twoᶜ · sucᶜ · `zero —→→ `suc `suc `zero
_ = begin
    twoᶜ · sucᶜ · `zero                     —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ "z" ⇒ sucᶜ · (sucᶜ · `"z")) · `zero  —→⟨ β-ƛ V-zero ⟩
    sucᶜ · (sucᶜ · `zero)                   —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
    sucᶜ · `suc `zero                       —→⟨ β-ƛ (V-suc V-zero) ⟩
    `suc `suc `zero                         ∎

_ : plus · one · one —→→ two
_ = begin
    plus · one · one                        —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
    _ · one · one                           —→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩
    _ · one                                 —→⟨ β-ƛ (V-suc V-zero) ⟩
    case one [zero⇒ one |suc "m" ⇒ `suc _ ] —→⟨ β-suc V-zero ⟩
    `suc (plus · `zero · one)               —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
    `suc (_ · `zero · one)                  —→⟨ ξ-suc (ξ-·₁ (β-ƛ V-zero)) ⟩
    `suc (_ · one)                          —→⟨ ξ-suc (β-ƛ (V-suc V-zero)) ⟩
    `suc _                                  —→⟨ ξ-suc β-zero ⟩
    `suc one                                ∎

infixr 7 _⇒_

data Type : Set where
    _⇒_ : Type → Type → Type
    `ℕ  : Type

infixl 5 _,_⦂_

data Context : Set where
    ∅     : Context
    _,_⦂_ : Context → Id → Type → Context

Context-≃ : Context ≃ List (Id × Type)
Context-≃ = record
    { to      = to
    ; from    = from
    ; from∘to = from∘to
    ; to∘from = to∘from
    }
    where
    to : Context → List (Id × Type)
    to ∅           = []
    to (Γ , x ⦂ A) = (x , A) ∷ to Γ

    from : List (Id × Type) → Context
    from []             = ∅
    from ((x , A) ∷ xs) = from xs , x ⦂ A

    from∘to : ∀ (x : Context) → from (to x) ≡ x
    from∘to ∅                             = refl
    from∘to (Γ , x ⦂ A) rewrite from∘to Γ = refl

    to∘from : ∀ (x : List (Id × Type)) → to (from x) ≡ x
    to∘from []                                = refl
    to∘from ((x , A) ∷ xs) rewrite to∘from xs = refl

infix 4 _⦂_∈_

data _⦂_∈_ : Id → Type → Context → Set where
    Z : ∀ {Γ : Context} {x : Id} {A : Type}
        -------------------
        → x ⦂ A ∈ Γ , x ⦂ A

    S : ∀ {Γ : Context} {x y : Id} {A B : Type}
        → x ≢ y
        → x ⦂ A ∈ Γ
        -------------------
        → x ⦂ A ∈ Γ , y ⦂ B

infix 4 _⊢_⦂_

data _⊢_⦂_ : Context → Term → Type → Set where
    -- Axiom.
    ⊢` : {Γ : Context} {x : Id} {A : Type}
        → x ⦂ A ∈ Γ
        -------------
        → Γ ⊢ ` x ⦂ A

    -- Arrow introduction.
    ⊢ƛ : ∀ {Γ : Context} {x : Id} {N : Term} {A B : Type}
        → Γ , x ⦂ A ⊢ N ⦂ B
        → Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B

    -- Arrow elimination.
    _·_ : ∀ {Γ : Context} {M N : Term} {A B : Type}
        → Γ ⊢ M ⦂ A ⇒ B
        → Γ ⊢ N ⦂ A
        ---------------
        → Γ ⊢ M · N ⦂ B

    -- Natural introduction 1.
    ⊢zero : ∀ {Γ : Context}
        ----------------
        → Γ ⊢ `zero ⦂ `ℕ

    -- Natural introduction 2.
    ⊢suc : ∀ {Γ : Context} {M : Term}
        → Γ ⊢ M ⦂ `ℕ
        -----------------
        → Γ ⊢ `suc M ⦂ `ℕ

    -- Natural elimination.
    ⊢case : ∀ {Γ : Context} {x : Id} {L M N : Term} {A : Type}
        → Γ ⊢ L ⦂ `ℕ
        → Γ ⊢ M ⦂ A
        → Γ , x ⦂ `ℕ ⊢ N ⦂ A
        --------------------------------------
        → Γ ⊢ case L [zero⇒ M |suc x ⇒ N ] ⦂ A

    ⊢μ : ∀ {Γ : Context} {x : Id} {M : Term} {A : Type}
        → Γ , x ⦂ A ⊢ M ⦂ A
        -------------------
        → Γ ⊢ μ x ⇒ M ⦂ A

Ch : Type → Type
Ch A = (A ⇒ A) ⇒ A ⇒ A

⊢twoᶜ : ∀ {Γ : Context} {A : Type} → Γ ⊢ twoᶜ ⦂ Ch A
⊢twoᶜ = ⊢ƛ (⊢ƛ (⊢` s · (⊢` s · ⊢` z)))
    where
    s = S (λ()) Z
    z = Z

⊢two : ∀ {Γ : Context} → Γ ⊢ two ⦂ `ℕ
⊢two = ⊢suc (⊢suc ⊢zero)

⊢plus : ∀ {Γ : Context} → Γ ⊢ plus ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ
⊢plus = ⊢μ (⊢ƛ (⊢ƛ (⊢case (⊢` m) (⊢` n) (⊢suc (⊢` + · ⊢` m' · ⊢` n')))))
    where
    + = S (λ()) (S (λ()) (S (λ()) Z))
    m = S (λ()) Z
    n = Z
    m' = Z
    n' = S (λ()) Z

⊢2+2 : ∀ {Γ : Context} → Γ ⊢ plus · two · two ⦂ `ℕ
⊢2+2 = ⊢plus · ⊢two · ⊢two

⊢plusᶜ : ∀ {Γ : Context} {A : Type} → Γ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A
⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` m · ⊢` s · (⊢` n · ⊢` s · ⊢` z)))))
    where
    m = S (λ()) (S (λ()) (S (λ()) Z))
    n = S (λ()) (S (λ()) Z)
    s = S (λ()) Z
    z = Z

⊢sucᶜ : ∀ {Γ : Context} → Γ ⊢ sucᶜ ⦂ `ℕ ⇒ `ℕ
⊢sucᶜ = ⊢ƛ (⊢suc (⊢` Z))

⊢2+2ᶜ : ∀ {Γ : Context} → Γ ⊢ plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ⦂ `ℕ
⊢2+2ᶜ = ⊢plusᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero

∈-injective : ∀ {Γ x A B} → x ⦂ A ∈ Γ → x ⦂ B ∈ Γ → A ≡ B
∈-injective Z        Z        = refl
∈-injective Z        (S x≢ _) = ⊥-elim (x≢ refl)
∈-injective (S x≢ _) Z        = ⊥-elim (x≢ refl)
∈-injective (S _ x)  (S _ y)  = ∈-injective x y

nope₁ : ∀ {Γ A} → ¬ (Γ ⊢ `zero · `suc `zero ⦂ A)
nope₁ (() · _)

nope₂ : ∀ {Γ A} → ¬ (Γ ⊢ ƛ "x" ⇒ `"x" · `"x" ⦂ A)
nope₂ (⊢ƛ (⊢` x · ⊢` x')) = contradiction (∈-injective x x')
    where
    contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A)
    contradiction ()

⊢mul : ∀ {Γ} → Γ ⊢ mul ⦂ `ℕ ⇒ `ℕ ⇒ `ℕ
⊢mul = ⊢μ (⊢ƛ (⊢ƛ (⊢case (⊢` m) ⊢zero (⊢plus · ⊢` n · (⊢` * · ⊢` m' · ⊢` n)))))
    where
    *  = S (λ()) (S (λ()) (S (λ()) Z))
    m  = S (λ()) Z
    m' = Z
    n  = S (λ()) Z

⊢mulᶜ : ∀ {Γ A} → Γ ⊢ mulᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A
⊢mulᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` m · (⊢` n · ⊢` s) · ⊢` z))))
    where
    m = S (λ()) (S (λ()) (S (λ()) Z))
    n = S (λ()) (S (λ()) Z)
    s = S (λ()) Z
    z = Z