Materials for my Haskell.SG talk on 9 November 2017

STLCSemantics.agda

module STLCSemantics where


--------------------------------------------------------------------------------


-- Types
infixr 7 _⇒_
data Type : Set
  where
    •    : Type
    _⇒_ : Type → Type → Type


-- Contexts
infixl 6 _,_
data Context : Set
  where
    ∅   : Context
    _,_ : Context → Type → Context


-- Variables
infix 4 _∋_
data _∋_ : Context → Type → Set
  where
    zero : ∀ {Γ A} → Γ , A ∋ A

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


-- Terms
infix 3 _⊢_
data _⊢_ : Context → Type → Set
  where
    var : ∀ {A Γ} → Γ ∋ A
                  ---------
                  → Γ ⊢ A

    lam : ∀ {A B Γ} → Γ , A ⊢ B
                    --------------
                    → Γ ⊢ A ⇒ B

    _$_ : ∀ {A B Γ} → Γ ⊢ A ⇒ B → Γ ⊢ A
                    ------------------------
                    → Γ ⊢ B


--------------------------------------------------------------------------------


open import Agda.Builtin.Unit public
  using (⊤ ; tt)


infixl 2 _×_
record _×_ (X : Set) (Y : Set) : Set
  where
    constructor _,_
    field
      proj₁ : X
      proj₂ : Y


--------------------------------------------------------------------------------


module Semantics1
  where
    -- Values
    ⟦_⟧ : Type → Set
    ⟦ • ⟧      = ⊤
    ⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧
     
     
    -- Environments
    ⟦_⟧⋆ : Context → Set
    ⟦ ∅ ⟧⋆     = ⊤
    ⟦ Γ , A ⟧⋆ = ⟦ Γ ⟧⋆ × ⟦ A ⟧

    lookup : ∀ {Γ A} → Γ ∋ A → ⟦ Γ ⟧⋆
                     ------------------
                     → ⟦ A ⟧
    lookup {∅}     ()      tt
    lookup {Γ , A} zero    (γ , a) = a
    lookup {Γ , B} (suc i) (γ , b) = lookup i γ
     
     
    -- Evaluation / reflection
    ↓ : ∀ {Γ A} → Γ ⊢ A → ⟦ Γ ⟧⋆
                -------------------
                → ⟦ A ⟧
    ↓ (var i) γ = lookup i γ
    ↓ (lam M) γ = λ a → ↓ M (γ , a)
    ↓ (M $ N) γ = (↓ M γ) (↓ N γ)
   
   
    mutual
      -- Universal reflection
      ↓ᵤ : ∀ {A Γ} → Γ ⊢ A
                   ---------
                   → ⟦ A ⟧
      ↓ᵤ {•}      M = tt
      ↓ᵤ {A ⇒ B} M = λ a → ↓ᵤ (M $ ↑ᵤ a)

      -- Universal reification
      ↑ᵤ : ∀ {A Γ} → ⟦ A ⟧
                   ---------
                   → Γ ⊢ A
      ↑ᵤ {•}      {Γ} tt = {!!}
      ↑ᵤ {A ⇒ B} {Γ} f  = lam (↑ᵤ (f (↓ᵤ {A} {Γ , A} (var zero))))
     
     
    -- Identity environment
    idₑ : ∀ {Γ} → ⟦ Γ ⟧⋆
    idₑ {∅}     = tt
    idₑ {Γ , A} = idₑ , ↓ᵤ {A} {Γ , A} (var zero)
     
     
    -- Inverse of evaluation / reification
    ↑ : ∀ {Γ A} → (⟦ Γ ⟧⋆ → ⟦ A ⟧)
                --------------------
                → Γ ⊢ A
    ↑ f = ↑ᵤ (f idₑ)


--------------------------------------------------------------------------------


-- Order-preserving embeddings / renamings
infix 4 _⊇_
data _⊇_ : Context → Context → Set
  where
    done : ∅ ⊇ ∅

    drop : ∀ {Γ Γ′ A} → Γ′ ⊇ Γ
                      -------------
                      → Γ′ , A ⊇ Γ

    keep : ∀ {Γ Γ′ A} → Γ′ ⊇ Γ
                      -----------------
                      → Γ′ , A ⊇ Γ , A


lookupᵣ : ∀ {Γ Γ′ A} → Γ′ ⊇ Γ → Γ ∋ A
                     ------------------
                     → Γ′ ∋ A
lookupᵣ done     i       = i
lookupᵣ (drop η) i       = suc (lookupᵣ η i)
lookupᵣ (keep η) zero    = zero
lookupᵣ (keep η) (suc i) = suc (lookupᵣ η i)


-- Identity renaming
idᵣ : ∀ {Γ} → Γ ⊇ Γ
idᵣ {∅}     = done
idᵣ {Γ , A} = keep idᵣ

-- Composition of renamings
_∘ᵣ_ : ∀ {Γ Γ′ Γ″} → Γ′ ⊇ Γ → Γ″ ⊇ Γ′
                   --------------------
                   → Γ″ ⊇ Γ
η      ∘ᵣ done    = η
η      ∘ᵣ drop η′ = drop (η ∘ᵣ η′)
drop η ∘ᵣ keep η′ = drop (η ∘ᵣ η′)
keep η ∘ᵣ keep η′ = keep (η ∘ᵣ η′)


-- Renaming of terms
rename : ∀ {Γ Γ′ A} → Γ′ ⊇ Γ → Γ ⊢ A
                    -------------------
                    → Γ′ ⊢ A

rename η (var i) = var (lookupᵣ η i)
rename η (lam M) = lam (rename (keep η) M)
rename η (M $ N) = rename η M $ rename η N


--------------------------------------------------------------------------------


module Semantics2
  where
    -- Values
    infix 3 _⊩_
    _⊩_ : Context → Type → Set
    W ⊩ •      = W ⊢ •
    W ⊩ A ⇒ B = W ⊩ A → W ⊩ B


    -- Relocation of values
    relocate : ∀ {A W W′} → W′ ⊇ W → W ⊩ A
                          -------------------
                          → W′ ⊩ A
    relocate {•}      η M = rename η M
    relocate {A ⇒ B} η f = λ a → {!!}
     
     
    -- Environments
    infix 3 _⊩⋆_
    _⊩⋆_ : Context → Context → Set
    W ⊩⋆ ∅     = ⊤
    W ⊩⋆ Γ , A = W ⊩⋆ Γ × W ⊩ A
     
    lookup : ∀ {Γ A W} → Γ ∋ A → W ⊩⋆ Γ
                       -------------------
                       → W ⊩ A
    lookup {∅}     ()      tt
    lookup {Γ , A} zero    (γ , a) = a
    lookup {Γ , B} (suc i) (γ , b) = lookup i γ


    -- Relocation of environments
    relocate⋆ : ∀ {Γ W W′} → W′ ⊇ W → W ⊩⋆ Γ
                           --------------------
                           → W′ ⊩⋆ Γ
    relocate⋆ {∅}     η tt      = tt
    relocate⋆ {Γ , A} η (γ , a) = relocate⋆ η γ , relocate η a
     
                   
    -- Evaluation / reflection  
    ↓ : ∀ {Γ A W} → Γ ⊢ A → W ⊩⋆ Γ
                  --------------------
                  → W ⊩ A
    ↓ (var i) γ = lookup i γ
    ↓ (lam M) γ = λ a → ↓ M (γ , a)
    ↓ (M $ N) γ = (↓ M γ) (↓ N γ)
   
   
    mutual
      -- Universal reflection
      ↓ᵤ : ∀ {A Γ} → Γ ⊢ A
                   ---------
                   → Γ ⊩ A
      ↓ᵤ {•}      M = M
      ↓ᵤ {A ⇒ B} M = λ a → ↓ᵤ (M $ ↑ᵤ a)

      -- Universal reification
      ↑ᵤ : ∀ {A Γ} → Γ ⊩ A
                   ---------
                   → Γ ⊢ A
      ↑ᵤ {•}      {Γ} M = M
      ↑ᵤ {A ⇒ B} {Γ} f = lam (↑ᵤ {!f ?!})
     
     
    -- Identity environment
    idₑ : ∀ {Γ} → Γ ⊩⋆ Γ
    idₑ {∅}     = tt
    idₑ {Γ , A} = relocate⋆ (drop idᵣ) idₑ , ↓ᵤ (var zero)
     
     
    -- Inverse of evaluation / reification
    ↑ : ∀ {Γ A} → (∀ {W} → W ⊩⋆ Γ → W ⊩ A)
                -------------------------------
                → Γ ⊢ A
    ↑ f = ↑ᵤ (f idₑ)


--------------------------------------------------------------------------------


module Semantics3
  where
    -- Values
    infix 3 _⊩_
    _⊩_ : Context → Type → Set
    W ⊩ •      = W ⊢ •
    W ⊩ A ⇒ B = ∀ {W′} → W′ ⊇ W → W′ ⊩ A
                         -------------------
                         → W′ ⊩ B


    -- Relocation of values
    relocate : ∀ {A W W′} → W′ ⊇ W → W ⊩ A
                          -------------------
                          → W′ ⊩ A
    relocate {•}      η M = rename η M
    relocate {A ⇒ B} η f = λ η′ a → f (η ∘ᵣ η′) a
     
     
    -- Environments
    infix 3 _⊩⋆_
    _⊩⋆_ : Context → Context → Set
    W ⊩⋆ ∅     = ⊤
    W ⊩⋆ Γ , A = W ⊩⋆ Γ × W ⊩ A
     
    lookup : ∀ {Γ A W} → Γ ∋ A → W ⊩⋆ Γ
                       -------------------
                       → W ⊩ A
    lookup {∅}     ()      tt
    lookup {Γ , A} zero    (γ , a) = a
    lookup {Γ , B} (suc i) (γ , b) = lookup i γ


    -- Relocation of environments
    relocate⋆ : ∀ {Γ W W′} → W′ ⊇ W → W ⊩⋆ Γ
                           --------------------
                           → W′ ⊩⋆ Γ
    relocate⋆ {∅}     η tt      = tt
    relocate⋆ {Γ , A} η (γ , a) = relocate⋆ η γ , relocate η a
     
     
    -- Evaluation / reflection
    ↓ : ∀ {Γ A W} → Γ ⊢ A → W ⊩⋆ Γ
                  --------------------
                  → W ⊩ A
    ↓ (var i) γ = lookup i γ
    ↓ (lam M) γ = λ η a → ↓ M (relocate⋆ η γ , a)
    ↓ (M $ N) γ = (↓ M γ) idᵣ (↓ N γ)
   
   
    mutual
      -- Universal reflection
      ↓ᵤ : ∀ {A Γ} → Γ ⊢ A
                   ---------
                   → Γ ⊩ A
      ↓ᵤ {•}      M = M
      ↓ᵤ {A ⇒ B} M = λ η a → ↓ᵤ (rename η M $ ↑ᵤ a)

      -- Universal reification
      ↑ᵤ : ∀ {A Γ} → Γ ⊩ A
                   ---------
                   → Γ ⊢ A
      ↑ᵤ {•}      {Γ} M = M
      ↑ᵤ {A ⇒ B} {Γ} f = lam (↑ᵤ (f (drop idᵣ) (↓ᵤ (var zero))))
     
     
    -- Identity environment
    idₑ : ∀ {Γ} → Γ ⊩⋆ Γ
    idₑ {∅}     = tt
    idₑ {Γ , A} = relocate⋆ (drop idᵣ) idₑ , ↓ᵤ (var zero)
     
     
    -- Inverse of evaluation / reification
    ↑ : ∀ {Γ A} → (∀ {W} → W ⊩⋆ Γ → W ⊩ A)
                → Γ ⊢ A
    ↑ f = ↑ᵤ (f idₑ)


    -- Normalisation-by-evaluation
    nbe : ∀ {Γ A} → Γ ⊢ A
                  ---------
                  → Γ ⊢ A
    nbe M = ↑ (↓ M)


--------------------------------------------------------------------------------


module Semantics4
  where
    -- Intuitionistic Kripke models
    record Model : Set₁
      where
        field
          -- Set of worlds
          World    : Set
          
          -- Family of ground sets
          Ground   : World → Set
          
          -- Accessibility relation
          _≥_      : World → World → Set
          
          -- Reflexivity of accessibility
          idₐ      : ∀ {W} → W ≥ W
          
          -- Transitivity of accessibility
          _∘ₐ_     : ∀ {W W′ W″} → W′ ≥ W → W″ ≥ W′
                                 --------------------
                                 → W″ ≥ W
                               
          -- Monotonicity of ground sets with respect to accessibility
          reground : ∀ {W W′} → W′ ≥ W → Ground W
                              ---------------------
                              → Ground W′
     
    open Model {{...}}


    -- Values
    infix 3 _⊩_
    _⊩_ : ∀ {{_ : Model}} → World → Type → Set
    W ⊩ •      = Ground W
    W ⊩ A ⇒ B = ∀ {W′} → W′ ≥ W → W′ ⊩ A
                         -------------------
                         → W′ ⊩ B


    -- Relocation of values
    relocate : ∀ {{_ : Model}} {A W W′} → W′ ≥ W → W ⊩ A
                                        -------------------
                                        → W′ ⊩ A
    relocate {•}      η M = reground η M
    relocate {A ⇒ B} η f = λ η′ a → f (η ∘ₐ η′) a
     
     
    -- Environments
    infix 3 _⊩⋆_
    _⊩⋆_ : ∀ {{_ : Model}} → World → Context → Set
    W ⊩⋆ ∅     = ⊤
    W ⊩⋆ Γ , A = W ⊩⋆ Γ × W ⊩ A
     
    lookup : ∀ {{_ : Model}} {Γ A W} → Γ ∋ A → W ⊩⋆ Γ
                                     -------------------
                                     → W ⊩ A
    lookup {∅}     ()      tt
    lookup {Γ , A} zero    (γ , a) = a
    lookup {Γ , B} (suc i) (γ , b) = lookup i γ


    -- Relocation of environments
    relocate⋆ : ∀ {{_ : Model}} {Γ W W′} → W′ ≥ W → W ⊩⋆ Γ
                                         --------------------
                                         → W′ ⊩⋆ Γ
    relocate⋆ {∅}     η tt      = tt
    relocate⋆ {Γ , A} η (γ , a) = relocate⋆ η γ , relocate {A} η a
     
     
    -- Evaluation / reflection
    ↓ : ∀ {{_ : Model}} {Γ A W} → Γ ⊢ A → W ⊩⋆ Γ
                                --------------------
                                → W ⊩ A
    ↓ (var i) γ = lookup i γ
    ↓ (lam M) γ = λ η a → ↓ M (relocate⋆ η γ , a)
    ↓ (M $ N) γ = (↓ M γ) idₐ (↓ N γ)


    -- Universal model
    instance
      canonical : Model
      canonical = record { World    = Context
                         ; Ground   = _⊢ •
                         ; _≥_      = _⊇_
                         ; idₐ      = idᵣ
                         ; _∘ₐ_     = _∘ᵣ_
                         ; reground = rename
                         }
   
    mutual
      -- Universal reflection
      ↓ᵤ : ∀ {A Γ} → Γ ⊢ A
                   ---------
                   → Γ ⊩ A
      ↓ᵤ {•}      M = M
      ↓ᵤ {A ⇒ B} M = λ η a → ↓ᵤ (rename η M $ ↑ᵤ a)

      -- Universal reification
      ↑ᵤ : ∀ {A Γ} → Γ ⊩ A
                   ---------
                   → Γ ⊢ A
      ↑ᵤ {•}      {Γ} M = M
      ↑ᵤ {A ⇒ B} {Γ} f = lam (↑ᵤ (f (drop idᵣ) (↓ᵤ {A} (var zero))))
     
     
    -- Identity environment
    idₑ : ∀ {Γ} → Γ ⊩⋆ Γ
    idₑ {∅}     = tt
    idₑ {Γ , A} = relocate⋆ (drop idᵣ) idₑ , ↓ᵤ {A} (var zero)
     
     
    -- Inverse of evaluation / reification
    ↑ : ∀ {Γ A} → (∀ {W} → W ⊩⋆ Γ → W ⊩ A)
                → Γ ⊢ A
    ↑ f = ↑ᵤ (f idₑ)


    -- Normalisation-by-evaluation
    nbe : ∀ {Γ A} → Γ ⊢ A
                  ---------
                  → Γ ⊢ A
    nbe M = ↑ (↓ M)


--------------------------------------------------------------------------------