Normalization by Evaluation for Simply Typed Lambda Calculus

Normalize.agda

module Normalize where

-- https://gist.github.com/rntz/2543cf9ef5ee4e3d990ce3485a0186e2
-- http://www.rntz.net/post/2019-01-18-binding-in-agda.html
-- Lean version: https://gist.github.com/pedrominicz/4ae448dc61d36ae0c806ba1bd3e8b538

open import Agda.Builtin.Equality
open import Data.Empty
open import Data.Sum
open import Function
open import Level using (Level; Lift; lift; lower; 0ℓ)

infixr 7 _⇒_
infixl 5 _,_

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

Context : Set₁
Context = Type → Set

∅ : Context
∅ A = ⊥

_,_ : Context → Type → Context
Γ , A = λ B → A ≡ B ⊎ Γ B

infix 4 _∈_ _⊢_

_∈_ : Type → Context → Set
A ∈ Γ = Γ A

pattern zero  = inj₁ refl
pattern suc x = inj₂ x

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

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

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

infix 4 _↓_ _↑_

data _↓_ : Context → Type → Set
data _↑_ : Context → Type → Set

-- Checking.
data _↓_ where
    ƛ : ∀ {Γ A B}
        → Γ , A ↓ B
        -----------
        → Γ ↓ A ⇒ B

    o : ∀ {Γ}
        → Γ ↑ o
        -------
        → Γ ↓ o

-- Synthesizing.
data _↑_ where
    ` : ∀ {Γ A}
        → A ∈ Γ
        -------
        → Γ ↑ A

    _·_ : ∀ {Γ A B}
        → Γ ↑ A ⇒ B
        → Γ ↓ A
        -----------
        → Γ ↑ B

infix 4 _⊆_

_⊆_ : Context → Context → Set
Γ ⊆ Δ = ∀ {A} → A ∈ Γ → A ∈ Δ

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

rename↓ : ∀ {Γ Δ A} → Γ ⊆ Δ → Γ ↓ A → Δ ↓ A
rename↑ : ∀ {Γ Δ A} → Γ ⊆ Δ → Γ ↑ A → Δ ↑ A
rename↓ {Γ} ρ (ƛ M) = ƛ (rename↓ (ext {Γ} ρ) M)
rename↓ ρ (o M)     = o (rename↑ ρ M)
rename↑ ρ (` x)     = ` (ρ x)
rename↑ ρ (M · N)   = rename↑ ρ M · rename↓ ρ N

-- The standard library should export this.
1ℓ : Level
1ℓ = Level.suc 0ℓ

[_⊢_] : Context → Type → Set₁
[ Γ ⊢ A ⇒ B ] = ∀ {Δ} → Γ ⊆ Δ → [ Δ ⊢ A ] → [ Δ ⊢ B ]
[ Γ ⊢ o ]     = Lift 1ℓ (Γ ↑ o)

reify   : ∀ {A Γ} → [ Γ ⊢ A ] → Γ ↓ A
reflect : ∀ {A Γ} → Γ ↑ A → [ Γ ⊢ A ]
reify   {A ⇒ B} ⊢M = ƛ (reify (⊢M suc (reflect (` zero))))
reify   {o}     ⊢M = o (lower ⊢M)
reflect {A ⇒ B} M  = λ ρ ⊢N → reflect (rename↑ ρ M · reify ⊢N)
reflect {o}     M  = lift M

rename : ∀ {Γ Δ} → Γ ⊆ Δ → ∀ {A} → [ Γ ⊢ A ] → [ Δ ⊢ A ]
rename ρ {A ⇒ B} ⊢M       = λ σ → ⊢M (σ ∘ ρ)
rename ρ {o}     (lift M) = lift (rename↑ ρ M)

[_⊢*_] : Context → Context → Set₁
[ Γ ⊢* Δ ] = ∀ {A} → A ∈ Δ → [ Γ ⊢ A ]

extend : ∀ {Γ Δ A} → [ Γ ⊢* Δ ] → [ Γ ⊢ A ] → [ Γ ⊢* Δ , A ]
extend ρ M zero    = M
extend ρ M (suc x) = ρ x

id* : ∀ {Γ} → [ Γ ⊢* Γ ]
id* x = reflect (` x)

denotation : ∀ {Γ Δ A} → Γ ⊢ A → [ Δ ⊢* Γ ] → [ Δ ⊢ A ]
denotation (` x)   ρ = ρ x
denotation (ƛ M)   ρ = λ σ x → denotation M (extend (rename σ ∘ ρ) x)
denotation (M · N) ρ = denotation M ρ id (denotation N ρ)

normalize : ∀ {Γ A} → Γ ⊢ A → Γ ↓ A
normalize M = reify (denotation M id*)