module Metaprog2016 where

open import Data.List using (List) renaming ([] to )
open import Data.Maybe using (Maybe)
open import Data.Product using (_×_)
open import Data.Unit using () renaming ( to 𝟙)




-- TOWARDS INTENSIONAL ANALYSIS OF SYNTAX
--
-- Miëtek Bak
-- mietek@bak.io
--
-- http://github.com/mietek/metaprog2016
--
-- International Summer School on Metaprogramming
-- Robinson College, Cambridge, 8th to 12th August 2016




-- Consider a basic fragment of intuitionistic modal logic S4 (IS4).

data Type : Set where
  _▻_ : Type  Type  Type
  _∧_ : Type  Type  Type
    : Type
  □_  : Type  Type

postulate
  _⊢_ : List Type  Type  Set

-- IS4 provides the logical foundations for MetaML.




-- Sheard (2001) reminds us that MetaML only allows syntax to be constructed
-- and executed at runtime.  Observation and decomposition is not supported.
--
-- “Accomplishments and research challenges in meta-programming”
-- http://dx.doi.org/10.1007/3-540-44806-3_2

postulate
       : Type
  yes   :  {Γ}    Γ  
  no    :  {Γ}    Γ  
  isApp :  {Γ A}  Γ  (( A)  )

-- Has anyone built a typed system supporting intensional analysis of syntax?




-- I don’t know, but Gabbay and Nanevski (2012) come close.  They give a
-- Tarski-style semantics for IS4, reading “□ A” as “closed syntax of type A”.
--
-- “Denotation of contextual modal type theory: Syntax and meta-programming”
-- http://dx.doi.org/10.1016/j.jal.2012.07.002

module GabbayNanevski2012 where
  ⊨_ : Type  Set
   (A  B) =  A   B
   (A  B) = ( A) × ( B)
         = 𝟙
   ( A)   = (  A) × ( A)

-- Can we construct a proof of completeness with respect to this semantics
-- and obtain normalisation by evaluation (NbE) for IS4?




-- Yes, we can!  As long as we also take from Coquand and Dybjer (1997).
--
-- “Intuitionistic model constructions and normalization proofs”
-- http://dx.doi.org/10.1017/S0960129596002150

module CoquandDybjer1997GabbayNanevski2012 where
  ⊨_ : Type  Set
   (A  B) = (  (A  B)) × ( A   B)
   (A  B) = ( A) × ( B)
         = 𝟙
   ( A)   = (  A) × ( A)

-- Could we perhaps read “□ A” as “open syntax of type A”?




-- I don’t know, but I’ve had an idea about that...

postulate
  _⊆_ : List Type  List Type  Set

module ??? where
  _⊨_ : List Type  Type  Set
  Δ  (A  B) =  {Δ′}  Δ  Δ′  Δ′  A  Δ′  B
  Δ  (A  B) = (Δ  A) × (Δ  B)
  Δ        = 𝟙
  Δ  ( A)   =  {Δ′}  Δ  Δ′  (Δ′  A) × (Δ′  A)

-- Does this look suspiciously like a Kripke-style possible worlds semantics?




-- Yes, it does!  We can find one of these in Alechina et al. (2001).
--
-- “Categorical and Kripke semantics for constructive S4 modal logic”
-- http://dx.doi.org/10.1007/3-540-44802-0_21

postulate
  World : Set
  _≤_   : World  World  Set
  _R_   : World  World  Set

module AlechinaMendlerDePaivaRitter2001 where
  _⊩_ : World  Type  Set
  w  (A  B) =  {w′}  w  w′  w′  A  w′  B
  w  (A  B) = (w  A) × (w  B)
  w        = 𝟙
  w  ( A)   =  {w′}  w  w′   {v′}  w′ R v′  v′  A

-- Has anyone constructed a proof of completeness with respect to a
-- Kripke-style semantics for IS4?




-- I haven’t found one, and I’ve tried five.

--           v′      w″  →   v″              w″
--           ◌───R───●   →   ◌───────R───────●
--           │           →   │
--           ≤  ξ′,ζ′    →   │
--   v       │           →   │
--   ◌───R───●           →   ≤
--   │       w′          →   │
--   ≤  ξ,ζ              →   │
--   │                   →   │
--   ●                   →   ●
--   w                   →   w

-- How do we go from being able to talk about open syntax to being able
-- to intensionally analyse syntax at runtime?




-- I don’t know, but I’ve noticed a funny coincidence...
--
-- Work in progress:
-- http://github.com/mietek/hilbert-gentzen




-- FIN