Programming Language Foundations in Agda: De Bruijn

DeBruijn.agda

module DeBruijn where

open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂)
open import Relation.Nullary using (¬_)

infixr 7 _⇒_
infixl 5 _,_

data Type : Set where
    _⇒_ : Type → Type → Type
    ∘   : Type

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

infix 4 _∈_
infix 4 _⊢_

data _∈_ : Type → Context → Set where
    zero : ∀ {Γ A}
        -----------
        → A ∈ Γ , A

    suc : ∀ {Γ A B}
        → A ∈ Γ
        -----------
        → A ∈ Γ , B

data _⊢_ : Context → Type → Set where
    ` : ∀ {Γ A}
        → A ∈ Γ
        -------
        → Γ ⊢ A

    -- Arrow introduction.
    ƛ : ∀ {Γ A B}
        → Γ , A ⊢ B
        -----------
        → Γ ⊢ A ⇒ B

    -- Arrow elimination.
    _·_ : ∀ {Γ A B}
        → Γ ⊢ A ⇒ B
        → Γ ⊢ A
        -----------
        → Γ ⊢ B

    ∘ : ∀ {Γ}
        -------
        → Γ ⊢ ∘

ext : ∀ {Γ Δ}
    → (∀ {A}   → A ∈ Γ     → A ∈ Δ)
    -----------------------------------
    → (∀ {A B} → A ∈ Γ , B → A ∈ Δ , B)
ext ρ zero    = zero
ext ρ (suc x) = suc (ρ x)

rename : ∀ {Γ Δ}
    → (∀ {A} → A ∈ Γ → A ∈ Δ)
    -------------------------
    → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (` x)   = ` (ρ x)
rename ρ (ƛ N)   = ƛ (rename (ext ρ) N)
rename ρ (L · M) = rename ρ L · rename ρ M
rename ρ ∘       = ∘

exts : ∀ {Γ Δ}
    → (∀ {A}   → A ∈ Γ     → Δ ⊢ A)
    -----------------------------------
    → (∀ {A B} → A ∈ Γ , B → Δ , B ⊢ A)
exts σ zero    = ` zero
exts σ (suc x) = rename suc (σ x)

subst : ∀ {Γ Δ}
    → (∀ {A} → A ∈ Γ → Δ ⊢ A)
    -------------------------
    → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
subst σ (` x)   = σ x
subst σ (ƛ N)   = ƛ (subst (exts σ) N)
subst σ (L · M) = subst σ L · subst σ M
subst σ ∘       = ∘

_[_] : ∀ {Γ A B}
    → Γ , B ⊢ A
    → Γ ⊢ B
    -----------
    → Γ ⊢ A
_[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N
    where
    σ : ∀ {A} → A ∈ Γ , B → Γ ⊢ A
    σ zero    = M
    σ (suc x) = ` x

data Value : ∀ {Γ A} → Γ ⊢ A → Set where
    ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
        -------------
        → Value (ƛ N)

    ∘ : ∀ {Γ}
        ---------------
        → Value (∘ {Γ})

infix 2 _—→_

data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
    ξ₁ : ∀ {Γ A B} {L L' : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
        → L —→ L'
        -----------------
        → L · M —→ L' · M

    ξ₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M' : Γ ⊢ A}
        → Value V
        → M —→ M'
        -----------------
        → V · M —→ V · M'

    β : ∀ {Γ A B} {N : Γ , A ⊢ B} {V : Γ ⊢ A}
        → Value V
        ----------------------
        → (ƛ N) · V —→ N [ V ]

data _—→*_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set where
    _∎ : ∀ {Γ A} (M : Γ ⊢ A)
        ---------
        → M —→* M

    _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
        → L —→ M
        → M —→* N
        ---------
        → L —→* N

data Progress {A} (M : ∅ ⊢ A) : Set where
    step : ∀ {N : ∅ ⊢ A}
        → M —→ N
        ------------
        → Progress M

    done :
        Value M
        ------------
        → Progress M

progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
progress (ƛ N) = done ƛ
progress (L · M) with progress L
... | step L—→L' = step (ξ₁ L—→L')
... | done ƛ with progress M
...     | step M—→M' = step (ξ₂ ƛ M—→M')
...     | done VM    = step (β VM)
progress ∘ = done ∘

data Eval : ∀ {A} → ∅ ⊢ A → Set where
    result : ∀ {A} {L N : ∅ ⊢ A}
        → L —→* N
        → Value N
        ---------
        → Eval L

{-
-- The termination checker fails in the following function. STLC is strongly
-- normalizing but the typechecker cannot see this.
eval : ∀ {A}
    → (L : ∅ ⊢ A)
    -------------
    → Eval L
eval L with progress L
... | done VL = result (L ∎) VL
... | step {M} L—→M with eval M
...     | result M—→*N VN = result (L —→⟨ L—→M ⟩ M—→*N) VN
-}

----------------
-- Properties --
----------------

V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A}
    → Value M
    ------------
    → ¬ (M —→ N)
V¬—→ ∘ = λ ()

det : ∀ {Γ A} {M M' M'' : Γ ⊢ A}
    → M —→ M'
    → M —→ M''
    ----------
    → M' ≡ M''
det (ξ₁ L—→L')    (ξ₁ L—→L'')    = cong₂ _·_ (det L—→L' L—→L'') refl
det (ξ₁ L—→L')    (ξ₂ VL M—→M'') = ⊥-elim (V¬—→ VL L—→L')
det (ξ₂ VL M—→M') (ξ₁ L—→L'')    = ⊥-elim (V¬—→ VL L—→L'')
det (ξ₂ _ M—→M')  (ξ₂ _ M—→M'')  = cong₂ _·_ refl (det M—→M' M—→M'')
det (ξ₂ VL M—→M') (β VM)         = ⊥-elim (V¬—→ VM M—→M')
det (β VM)        (ξ₂ VL M—→M'') = ⊥-elim (V¬—→ VM M—→M'')
det (β _)         (β _)          = refl