DTMF.agda

{-

An unholy mix of

• Conor McBride, “Dependently typed metaprogramming”
  http://www.cl.cam.ac.uk/~ok259/agda-course-13/

• Oleg Kiselyov, “Typed tagless final interpreters”
  http://okmij.org/ftp/tagless-final/course/

and my own brand of crazy.

-}

-- NOTE: Temporary!
{-# OPTIONS --type-in-type #-}

module DTMF where

open import Data.List                             using ( List ; [] ; _∷_ )
open import Data.Nat                              using ( ℕ ; _+_ ; zero ; suc )
open import Data.Nat.Show                         using ( ) renaming ( show to showₙ )
open import Data.Product                          using ( _×_ ; _,_ )
open import Data.String                           using ( String ; _++_ )
open import Data.Unit                             using ( ⊤ ; tt )
open import Relation.Binary.Core                  using ( _≡_ ; refl )
open import Relation.Binary.PropositionalEquality using ( subst )




-- Syntax

data Ty : Set₁ where
  △_  : Set
      → Ty
  _⊃_ : Ty → Ty
           → Ty


data Cx (X : Set) : Set₁ where
  ε   : Cx X
  _,_ : Cx X → X
             → Cx X


data _∈_ (τ : Ty) : Cx Ty
                  → Set₁ where
  vz : ∀{Γ} → τ ∈ (Γ , τ)
  vs : ∀{Γ σ} → τ ∈ Γ
              → τ ∈ (Γ , σ)


-- Conor’s fish & chips

_⋉_ : Cx Ty → List Ty
            → Cx Ty
Γ ⋉ []       = Γ
Γ ⋉ (τ ∷ τs) = (Γ , τ) ⋉ τs


weak : ∀{Γ τ} → (τs : List Ty) → τ ∈ Γ
                               → τ ∈ (Γ ⋉ τs)
weak []       i = i
weak (_ ∷ τs) i = weak τs (vs i)


_⋊_ : Cx Ty → List Ty
            → List Ty
ε       ⋊ τs = τs
(Γ , τ) ⋊ τs = Γ ⋊ (τ ∷ τs)


revlem : (Γ : Cx Ty) → (τs : List Ty)
                     → ε ⋉ (Γ ⋊ τs) ≡ Γ ⋉ τs
revlem ε       τs = refl
revlem (Γ , σ) τs = revlem Γ (σ ∷ τs)


lem : (Δ Γ : Cx Ty) (τs : List Ty) → Δ ⋊ [] ≡ Γ ⋊ τs
                                   → Γ ⋉ τs ≡ Δ
lem Δ ε       .(Δ ⋊ []) refl = revlem Δ []
lem Δ (Γ , σ) τs        q    = lem Δ Γ (σ ∷ τs) q


module Conor (_⊢_ : Cx Ty → Ty → Set)
             (var : ∀{Γ τ} → τ ∈ Γ → Γ ⊢ τ)
             (lam : ∀{Γ σ τ} → (Γ , σ) ⊢ τ → Γ ⊢ (σ ⊃ τ)) where
  lambda : ∀{Γ σ τ}
         → ( ( ∀{Δ τs}{{_ : Δ ⋊ [] ≡ Γ ⋊ (σ ∷ τs)}}
             → Δ ⊢ σ
             )
           → (Γ , σ) ⊢ τ
           )
         → Γ ⊢ (σ ⊃ τ)
  lambda {Γ} f = lam (f \{Δ τs}{{q}} → subst (\Γ → Γ ⊢ _) (lem Δ Γ (_ ∷ τs) q) (var (weak τs vz)))




-- Evaluation toolkit

⟦_⟧T : Ty
     → Set
⟦ △ X ⟧T   = X
⟦ σ ⊃ τ ⟧T = ⟦ σ ⟧T → ⟦ τ ⟧T


⟦_⟧C : Cx Ty → (Ty → Set)
          → Set
⟦ ε ⟧C     V = ⊤
⟦ Γ , τ ⟧C V = ⟦ Γ ⟧C V × V τ


⟦_⟧∈ : ∀{Γ τ V} → τ ∈ Γ → ⟦ Γ ⟧C V
                        → V τ
⟦ vz ⟧∈   (G , t) = t
⟦ vs i ⟧∈ (G , t) = ⟦ i ⟧∈ G


-- Quotation toolkit

⟪_⟫∈ : ∀{Γ τ} → τ ∈ Γ → ℕ
                      → String
⟪ vz ⟫∈   n = "x" ++ showₙ n
⟪ vs i ⟫∈ n = ⟪ i ⟫∈ n




-- Term representation with higher-order abstract syntax (HOAS)
-- http:/okmij.org/ftp/tagless-final/course/TTF.hs

module HO where
  record Sym (⊩_ : Ty → Set) : Set where
    field
      nat : ℕ
          → ⊩ △ ℕ
      add : ⊩ △ ℕ → ⊩ △ ℕ
                  → ⊩ △ ℕ
      lam : ∀{σ τ} → (⊩ σ → ⊩ τ)
                   → ⊩ (σ ⊃ τ)
      app : ∀{σ τ} → ⊩ (σ ⊃ τ) → ⊩ σ
                               → ⊩ τ
  open Sym {{...}} public

  ⊫_ : Ty → Set₁
  ⊫ τ = ∀{⊩_ : Ty → Set}{{_ : Sym ⊩_}} → ⊩ τ

  module X where
    x₁ : ⊫ △ ℕ
    x₁ = add (nat 1) (nat 2)

    x₂ : ⊫ (△ ℕ ⊃ △ ℕ)
    x₂ = lam (\n → add n n)

    x₃ : ⊫ ((△ ℕ ⊃ △ ℕ) ⊃ △ ℕ)
    x₃ = lam (\f → add (app f (nat 1)) (nat 2))
    

  -- Evaluation

  module Eval where
    record ⊩_ (τ : Ty) : Set where
      constructor E
      field
        ⟦_⟧ : ⟦ τ ⟧T
    open ⊩_ public

    instance symE : Sym ⊩_
    Sym.nat symE n   = E n
    Sym.add symE m n = E (⟦ m ⟧ + ⟦ n ⟧)
    Sym.lam symE f   = E \x → ⟦ f (E x) ⟧
    Sym.app symE f x = E (⟦ f ⟧ ⟦ x ⟧)

    eval : ∀{τ} → ⊩ τ
                → ⟦ τ ⟧T
    eval x = ⟦ x ⟧
  
    module EX where
      x₁  = eval X.x₁
      x₂  = eval X.x₂
      x₂′ = eval X.x₂ 21
      x₃  = eval X.x₃


  -- Quotation

  module Show where
    record ⊩_ (τ : Ty) : Set where
      constructor S
      field
        ⟪_⟫ : ℕ
            → String
    open ⊩_ public

    instance symS : Sym ⊩_
    Sym.nat symS n   = S \_ → showₙ n
    Sym.add symS m n = S \k → "(" ++ ⟪ m ⟫ k ++ " + " ++ ⟪ n ⟫ k ++ ")"
    Sym.lam symS f   = S \k → let v = "x" ++ showₙ k in
                              "(λ" ++ v ++ " → " ++ ⟪ f (S \_ → v) ⟫ (k + 1) ++ ")"
    Sym.app symS f x = S \k → "(" ++ ⟪ f ⟫ k ++ " " ++ ⟪ x ⟫ k ++ ")"

    show : ∀{τ} → ⊩ τ
                → String
    show x = ⟪ x ⟫ 0
  
    module SX where
      x₁ = show X.x₁
      x₂ = show X.x₂
      x₃ = show X.x₃




-- Term representation with typed de Bruijn indices
-- http://okmij.org/ftp/tagless-final/course/TTFdB.hs

module DB where
  record Sym (_⊢_ : Cx Ty → Ty → Set) : Set₁ where
    field
      nat : ∀{Γ} → ℕ
                 → Γ ⊢ △ ℕ
      add : ∀{Γ} → Γ ⊢ △ ℕ → Γ ⊢ △ ℕ
                           → Γ ⊢ △ ℕ
      var : ∀{Γ τ} → τ ∈ Γ
                   → Γ ⊢ τ
      lam : ∀{Γ σ τ} → (Γ , σ) ⊢ τ
                     → Γ ⊢ (σ ⊃ τ)
      app : ∀{Γ σ τ} → Γ ⊢ (σ ⊃ τ) → Γ ⊢ σ
                                   → Γ ⊢ τ
    open Conor _⊢_ var lam public
  open Sym {{...}} public

  _⊨_ : Cx Ty → Ty → Set₁
  Γ ⊨ τ = ∀{_⊢_ : Cx Ty → Ty → Set}{{_ : Sym _⊢_}} → Γ ⊢ τ

  module X where
    x₁  : ∀{Γ} → Γ ⊨ △ ℕ
    x₁  = add (nat 1) (nat 2)

    x₂  : ∀{Γ} → Γ ⊨ (△ ℕ ⊃ △ ℕ)
    x₂  = lam (add (var vz) (var vz))

    x₂o : ∀{Γ} → (Γ , △ ℕ) ⊨ (△ ℕ ⊃ △ ℕ) -- Open term
    x₂o = lam (add (var vz) (var (vs vz)))

    x₃  : ∀{Γ} → Γ ⊨ ((△ ℕ ⊃ △ ℕ) ⊃ △ ℕ)
    x₃  = lam (add (app (var vz) (nat 1)) (nat 2))

  module ConorX where
    x₂ : ∀{Γ} → Γ ⊨ (△ ℕ ⊃ △ ℕ)
    x₂ = lambda (\n → add n n)

    x₃ : ∀{Γ} → Γ ⊨ ((△ ℕ ⊃ △ ℕ) ⊃ △ ℕ)
    x₃ = lambda (\f → add (app f (nat 1)) (nat 2))


  -- Evaluation

  module Eval where
    record _⊢_ (Γ : Cx Ty) (τ : Ty) : Set where
      constructor E
      field
        ⟦_⟧ : ⟦ Γ ⟧C ⟦_⟧T
            → ⟦ τ ⟧T
    open _⊢_ public
 
    instance symE : Sym _⊢_
    Sym.nat symE n   = E \_ → n
    Sym.add symE m n = E \G → ⟦ m ⟧ G + ⟦ n ⟧ G
    Sym.var symE i   = E \G → ⟦ i ⟧∈ G
    Sym.lam symE l   = E \G → \x → ⟦ l ⟧ (G , x)
    Sym.app symE f x = E \G → ⟦ f ⟧ G (⟦ x ⟧ G)

    eval : ∀{τ} → ε ⊢ τ
                → ⟦ τ ⟧T
    eval x = ⟦ x ⟧ tt

    module EX where
      x₁  = eval X.x₁
      x₂  = eval X.x₂
      x₂′ = eval X.x₂ 21
      x₃  = eval X.x₃


  -- Quotation

  module Show where
    record _⊢_ (Γ : Cx Ty) (τ : Ty) : Set where
      constructor S
      field
        ⟪_⟫ : ℕ
            → String
    open _⊢_ public

    instance symS : Sym _⊢_
    Sym.nat symS n   = S \_ → showₙ n
    Sym.add symS m n = S \k → "(" ++ ⟪ m ⟫ k ++ " + " ++ ⟪ n ⟫ k ++ ")"
    Sym.var symS i   = S \k → ⟪ i ⟫∈ k
    Sym.lam symS l   = S \k → let v = "x" ++ showₙ k in
                              "(λ" ++ v ++ " → " ++ ⟪ l ⟫ (k + 1) ++ ")"
    Sym.app symS f x = S \k → "(" ++ ⟪ f ⟫ k ++ " " ++ ⟪ x ⟫ k ++ ")"

    show : ∀{τ} → ε ⊢ τ
                → String
    show x = ⟪ x ⟫ 0

    module SX where
      x₁ = show X.x₁
      x₂ = show X.x₂
      x₃ = show X.x₃




-- Transformation from de Bruijn to HOAS
-- http://okmij.org/ftp/tagless-final/course/TTFdBHO.hs

module DBtoHO where
  record _▶_⊢_ (⊩_ : Ty → Set) (Γ : Cx Ty) (τ : Ty) : Set where
    constructor T
    field
      ⟦_⟧ : ⟦ Γ ⟧C ⊩_
          → ⊩ τ
  open _▶_⊢_ public
  open HO.Sym {{...}}
  
  instance symT : ∀{⊩_}{{_ : HO.Sym ⊩_}} → DB.Sym (_▶_⊢_ ⊩_)
  DB.Sym.nat symT n   = T \_ → nat n
  DB.Sym.add symT m n = T \G → add (⟦ m ⟧ G) (⟦ n ⟧ G)
  DB.Sym.var symT i   = T \G → ⟦ i ⟧∈ G
  DB.Sym.lam symT l   = T \G → lam \x → ⟦ l ⟧ (G , x)
  DB.Sym.app symT f x = T \G → app (⟦ f ⟧ G) (⟦ x ⟧ G)

  run : ∀{⊩_ τ} → ⊩_ ▶ ε ⊢ τ
                → ⊩ τ
  run x = ⟦ x ⟧ tt

  eval : ∀{τ} → HO.Eval.⊩_ ▶ ε ⊢ τ
              → ⟦ τ ⟧T
  eval tx = HO.Eval.eval (run tx)
    
  show : ∀{τ} → HO.Show.⊩_ ▶ ε ⊢ τ
              → String
  show tx = HO.Show.show (run tx)

  module EX where
    x₁ = eval DB.X.x₁
    x₂ = eval DB.X.x₂
    x₃ = eval DB.X.x₃

  module SX where
    x₁ = show DB.X.x₁
    x₂ = show DB.X.x₂
    x₃ = show DB.X.x₃





-- Transformation from HOAS to de Bruijn
-- (in progress)

module HOtoDB where
  record _▶⊩_ (_⊢_ : Cx Ty → Ty → Set) (τ : Ty) : Set where
    constructor T
    field
      ⟦_⟧ : ∀{Γ} → Γ ⊢ τ
  open _▶⊩_
  open DB.Sym {{...}}

  instance symT : ∀{_⊢_}{{_ : DB.Sym _⊢_}} → HO.Sym (_▶⊩_ _⊢_)
  HO.Sym.nat symT n       = T (nat n)
  HO.Sym.add symT m n     = T (add ⟦ m ⟧ ⟦ n ⟧)
  HO.Sym.lam symT f       = T (lambda \x → ⟦ f (T x) ⟧)
  HO.Sym.app symT f x     = T (app ⟦ f ⟧ ⟦ x ⟧)

  run : ∀{_⊢_ τ} → _⊢_ ▶⊩ τ
                 → ε ⊢ τ
  run x = ⟦ x ⟧

  eval : ∀{τ} → DB.Eval._⊢_ ▶⊩ τ
              → ⟦ τ ⟧T
  eval tx = DB.Eval.eval (run tx)

  show : ∀{τ} → DB.Show._⊢_ ▶⊩ τ
              → String
  show tx = DB.Show.show (run tx)

  module EX where
    x₁ = eval HO.X.x₁
    x₂ = eval HO.X.x₂
    x₃ = eval HO.X.x₃

  module SX where
    x₁ = show HO.X.x₁
    x₂ = show HO.X.x₂
    x₃ = show HO.X.x₃