Programming Language Foundations in Agda: Inference

Inference.agda

module Inference where

open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Relation.Binary.PropositionalEquality
    using (_≡_; _≢_; refl)
open import Relation.Nullary using (¬_; Dec; yes; no)

infixr 7 _⇒_
infixl 5 _,_

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

_≟_ : ∀ (A B : Type) → Dec (A ≡ B)
(A ⇒ B) ≟ (A' ⇒ B') with A ≟ A' | B ≟ B'
... | yes refl | yes refl = yes refl
... | no ¬A    | _        = no λ { refl → ¬A refl }
... | _        | no ¬B    = no λ { refl → ¬B refl }
⊤       ≟ ⊤       = yes refl
(A ⇒ B) ≟ ⊤       = no λ ()
⊤       ≟ (A ⇒ B) = no λ ()

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

data Term⁺ : Set
data Term⁻ : Set

data Term⁺ where
    `   : ℕ → Term⁺
    _·_ : Term⁺ → Term⁻ → Term⁺
    _↓_ : Term⁻ → Type → Term⁺

data Term⁻ where
    ƛ  : Term⁻ → Term⁻
    tt : Term⁻
    _↑ : Term⁺ → Term⁻

infix 4 _⦂_∈_

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

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

infix 4 _⊢_↑_
infix 4 _⊢_↓_

data _⊢_↑_ : Context → Term⁺ → Type → Set
data _⊢_↓_ : Context → Term⁻ → Type → Set

data _⊢_↑_ where
    ` : ∀ {Γ A x}
        → x ⦂ A ∈ Γ
        -------------------
        → Γ ⊢ ` x ↑ A

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

    _↓ : ∀ {Γ M A}
        → Γ ⊢ M ↓ A
        -----------------
        → Γ ⊢ (M ↓ A) ↑ A

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

    tt : ∀ {Γ}
        ------------
        → Γ ⊢ tt ↓ ⊤

    _↑_ : ∀ {Γ M A B}
        → Γ ⊢ M ↑ A
        → A ≡ B
        ---------------
        → Γ ⊢ (M ↑) ↓ B

unique↑ : ∀ {Γ M A B}
    → Γ ⊢ M ↑ A
    → Γ ⊢ M ↑ B
    -----------
    → A ≡ B
unique↑ (` x) (` x') = helper x x'
    where
    helper : ∀ {Γ A B x}
        → x ⦂ A ∈ Γ
        → x ⦂ B ∈ Γ
        ------------
        → A ≡ B
    helper zero    zero     = refl
    helper (suc x) (suc x') = helper x x'
unique↑ (M · N) (M' · N') = helper (unique↑ M M')
    where
    helper : ∀ {A A' B B'} → A ⇒ B ≡ A' ⇒ B' → B ≡ B'
    helper refl = refl
unique↑ (M ↓)   (M' ↓)    = refl

lookup : ∀ Γ x
    → Dec (∃[ A ] (x ⦂ A ∈ Γ))
lookup ∅       x    = no λ ()
lookup (Γ , A) zero = yes ⟨ A , zero ⟩
lookup (Γ , A) (suc x) with lookup Γ x
... | yes ⟨ A' , x' ⟩ = yes ⟨ A' , suc x' ⟩
... | no ¬∃ = no (ext∈ ¬∃)
    where
    ext∈ : ∀ {Γ B x}
        → ¬ ∃[ A ] (x ⦂ A ∈ Γ)
        ------------------------------
        → ¬ ∃[ A ] (suc x ⦂ A ∈ Γ , B)
    ext∈ ¬∃ ⟨ A , suc x ⟩ = ¬∃ ⟨ A , x ⟩

synthesize : ∀ Γ M
    --------------------------
    → Dec (∃[ A ] (Γ ⊢ M ↑ A))

inherit : ∀ Γ M A
    -----------------
    → Dec (Γ ⊢ M ↓ A)

synthesize Γ (` x) with lookup Γ x
... | yes ⟨ A , x' ⟩ = yes ⟨ A , ` x' ⟩
... | no ¬∃          = no λ { ⟨ A , ` x' ⟩ → ¬∃ ⟨ A , x' ⟩ }
synthesize Γ (M · N) with synthesize Γ M
... | no ¬∃          = no λ { ⟨ _ , M' · _ ⟩ → ¬∃ ⟨ _ , M' ⟩ }
... | yes ⟨ ⊤ , M' ⟩ = no λ { ⟨ _ , M'' · _ ⟩ → helper (unique↑ M' M'') }
    where
    helper : ∀ {A B} → ⊤ ≢ A ⇒ B
    helper ()
... | yes ⟨ A ⇒ B , M' ⟩ with inherit Γ N A
...     | yes N' = yes ⟨ B , M' · N' ⟩
...     | no ¬N' = no (helper M' ¬N')
        where
        -- Yes, this is a Hunter×Hunter reference.
        helper×helper : ∀ {A A' B B'} → A ⇒ B ≡ A' ⇒ B' → A ≡ A'
        helper×helper refl = refl

        helper : ∀ {Γ A B M N}
            → Γ ⊢ M ↑ A ⇒ B
            → ¬ (Γ ⊢ N ↓ A)
            --------------------------
            → ¬ ∃[ B ] (Γ ⊢ M · N ↑ B)
        helper M' ¬N' ⟨ B' , M'' · N' ⟩
            rewrite helper×helper (unique↑ M' M'') = ¬N' N'
synthesize Γ (M ↓ A) with inherit Γ M A
... | yes M' = yes ⟨ A , M' ↓ ⟩
... | no ¬M' = no λ { ⟨ _ , M' ↓ ⟩ → ¬M' M' }

inherit Γ (ƛ M) (A ⇒ B) with inherit (Γ , A) M B
... | yes M' = yes (ƛ M')
... | no ¬M' = no λ { (ƛ M') → ¬M' M' }
inherit Γ (ƛ M) ⊤       = no λ ()
inherit Γ tt    ⊤       = yes tt
inherit Γ tt    (A ⇒ B) = no λ ()
inherit Γ (M ↑) A with synthesize Γ M
... | no ¬∃ = no λ { (M' ↑ _) → ¬∃ ⟨ _ , M' ⟩ }
... | yes ⟨ A' , M' ⟩ with A' ≟ A
...     | yes refl = yes (M' ↑ refl)
...     | no ¬A≡A' = no (helper M' ¬A≡A')
        where
        helper : ∀ {Γ M' A A'}
            → Γ ⊢ M' ↑ A
            → A ≢ A'
            ---------------------
            → ¬ (Γ ⊢ (M' ↑) ↓ A')
        helper M' ¬A≡A' (M'' ↑ A≡A') rewrite unique↑ M' M'' = ¬A≡A' A≡A'