stlc-model5.agda

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ; _+_; suc)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product
open import Data.Fin hiding (suc; strengthen) renaming (_+_ to _Fin+_)
open import Data.Vec
open import Relation.Binary.PropositionalEquality

-- A notion of model of STLC
-- A Theory for STLC
-- A Syntax (of closed terms) for STLC
record Theory {l k : Level} : Set (lsuc (l ⊔ k)) where
  field
    -- Terms
    Tm : Set k
    -- Types
    Ty : Set l

    -- A typing relation

    -- Let's go PHOAS
    V : Ty -> Set k

    _∈_ : Tm -> Ty -> Set (l ⊔ k)

    -- A representation of False, required if I wish to prove consistency as a logic.
    False : Ty
    False-uninhabit : ∀ M -> ¬ (M ∈ False)

    Base : Ty
    base : Tm

    app : Tm -> Tm -> Tm
    lam : (A : Ty) -> (V A -> Tm) -> Tm

    Fun : Ty -> Ty -> Ty

    -- Semantic typing of open terms
    Fun-I : ∀  {A B} ->
      {f : V A -> Tm} ->
      ((x : V A) -> ((f x) ∈ B)) ->
      ------------------------------
      ((lam A f) ∈ (Fun A B))

    Fun-E : ∀ {M N A B} ->
      (M ∈ (Fun A B)) -> (N ∈ A) ->
      ------------------------------
      (app M N) ∈ B

    Base-I :
      -----------
      base ∈ Base

    var : ∀ {A} -> V A -> Tm
    Var : ∀ {A} ->
      (x : V A) ->
      -----------
      (var x) ∈ A

    reflect : ∀ {e A} -> (e ∈ A) -> V A

    -- should have some equations here if I care about, you know, terms
    _≡lc_ : ∀ {e e' A} -> (e ∈ A) -> (e' ∈ A) -> Set (l ⊔ k)

    -- equations are actually only about well-typed terms, or derivations, or ..
    -- representations of terms?
    Fun-β : ∀ {e A B} {f : V A -> Tm} ->
      (Df : ((x : V A) -> ((f x) ∈ B))) ->
      (Da : (e ∈ A)) ->
     ---------------------------------
     (Fun-E (Fun-I Df) Da) ≡lc (Df (reflect Da))

    Fun-η : ∀ {e A B} ->
      (Df : (e ∈ Fun A B)) ->
      ---------------------------------
      Df ≡lc (Fun-I (λ x -> Fun-E Df (Var x)))

-- How do we work with this syntax?
-- Well, for an arbirary model...
module Test {l k : Level} (model : Theory {l} {k}) where
  open Theory (model)
  -- (model._∈_) model.base model.Base
  -- well-typed unit
  example1 : base ∈ Base
  example1 = Base-I

  -- the Base -> Base function
  example2 : (lam Base (λ x -> var x)) ∈ (Fun Base Base)
  example2 = Fun-I (λ x -> (Var x))

  -- application of it
  example3 : (app (lam Base (λ x -> (var x))) base) ∈ Base
  example3 = Fun-E (Fun-I (λ x -> (Var x))) Base-I

-- Let's build some models.
module Model where
  -- I'll represent types as syntactic types...
  data STLC-Type : Set where
    STLC-False : STLC-Type
    STLC-Base : STLC-Type
    STLC-Fun : STLC-Type -> STLC-Type -> STLC-Type

  -- And well-typed terms as terms of the corresponding Agda type
  El : STLC-Type -> Set
  El STLC-False = ⊥
  El STLC-Base = ⊤
  El (STLC-Fun A B) = El A -> El B

  open Theory {{...}}
  -- M is a model of the Theory
  M : Theory
  -- terms don't matter; only derivations do
  -- this is kind of weird.. but kind of not?
  M .Tm = ⊤
  M .Ty = STLC-Type
  M .V A = El A
  -- the typing relation is interpreted in the reader monad for the Agda
  -- interpretation of the syntactic type.
  M ._∈_ e A = El A

  M .False = STLC-False
  M .False-uninhabit _ x = x

  M .Base = STLC-Base
  M .base = tt
  M .Base-I = tt

  M .Fun = STLC-Fun
  M .lam A f = tt
  M .app e1 e2 = tt

  -- Function introduction introduces an Agda function
  -- This is a little strange... the argument is already closed, but the fauxAS
  -- expects an argument that might be open?
  --
  -- AH! Actually, after changing the rule to require a closed argument, it
  -- expects an argument that isn't open (up to equivalence)
  -- This seems necessary to validate β/η
  M .Fun-I f arg = (f arg)
  -- Function elimination applies the underlying Agda function
  M .Fun-E Df Darg = Df Darg

  M .var m = tt
  M .Var = λ x -> x

  M .reflect = λ x -> x

  -- syntactic equality is propositional equality, and validates β/η
  M ._≡lc_ = _≡_
  M .Fun-β Df Da = refl
  M .Fun-η Df = refl

  -- Now we compile some of our examples to Agda using this model
  module TestAgda = Test M
  test1 : ⊤
  -- example requires the environment of the (0) free variables
  test1 = TestAgda.example1

  test2 : ⊤
  test2 = TestAgda.example2 tt


-- inital model
module Initial where
  ---- well-bound syntax
  --data Syn : (n : ℕ) -> Set where
  --  `base : ∀ {n} -> Syn n
  --  `lam : ∀ {n} -> (Syn (ℕ.suc n)) -> Syn n
  --  `app : ∀ {n} -> Syn n -> Syn n -> Syn n
  --  `var : ∀ {n} -> Fin n -> Syn n
  -- Using well-bound syntax seems to complicated things

  -- syntax
  data Syn : Set where
    `base : Syn
    `lam : Syn -> Syn
    `app : Syn -> Syn -> Syn
    `var : {n : ℕ} -> (Fin n) -> Syn

  data `Type : Set where
    `False : `Type
    `Base : `Type
    `Fun : `Type -> `Type -> `Type

  SEnv = Vec `Type

  shift : ℕ -> Syn -> Syn
  shift n `base = `base
  shift ℕ.zero (`lam e) = `lam e
  shift (suc n) (`lam e) = `lam (shift n e)
  shift n (`app e e') = `app (shift n e) (shift n e')
  shift n (`var x) = `var ((fromℕ n) Fin+ x)

  data _⊢_::_ : ∀ {n} -> SEnv n -> Syn -> `Type -> Set where
    IVar : ∀ {A} {n : ℕ} {Γ : SEnv n} ->
      (m : Fin n) ->
      (A ≡ (lookup Γ m)) ->
      -------------------------
      Γ ⊢ `var m :: A

    IFun-I : ∀ {n} {Γ : SEnv n} {e A B} ->
      (A ∷ Γ) ⊢ e :: B ->
      ----------------------
      Γ ⊢ `lam e :: `Fun A B

    IFun-E : ∀ {n} {Γ : SEnv n} {A B e1 e2} ->
      Γ ⊢ e1 :: `Fun A B ->
      Γ ⊢ e2 :: A ->
      ------------------
      Γ ⊢ `app e1 e2 :: B

    IBase-I : ∀ {n} {Γ : SEnv n} ->
      ----------------
      Γ ⊢ `base :: `Base

    IWeakenL : ∀ {n} {Γ : SEnv n} {e A B} ->
      Γ ⊢ e :: B ->
      ---------------
      (A ∷ Γ) ⊢ (shift 1 e) :: B

  WeakenL : ∀ {n m e B} {Γ : SEnv n} {Γ' : SEnv m} ->
    (Γ ⊢ e :: B) ->
    -- Needs to be
    -- Γ ⊢ (shift m e) :: B ->
    -- But then I can't actually finish the model.
    -- So NB: Something is Wrong
    ((Γ' ++ Γ) ⊢ e :: B)
  WeakenL (IVar m x) = {!!}
  WeakenL (IFun-I D) = {!!}
  WeakenL (IFun-E D D₁) = {!!}
  WeakenL IBase-I = {!!}
  WeakenL (IWeakenL D) = {!!}

  WeakenR : ∀ {n m e B} {Γ : SEnv n} {Γ' : SEnv m} ->
    (Γ ⊢ e :: B) ->
    ((Γ ++ Γ') ⊢ e :: B)

  close : Syn -> Syn -> Syn
  isubst : ∀ {n} {Γ : SEnv n} {A e B e'} -> ((A ∷ Γ) ⊢ e :: B) -> (Γ ⊢ e' :: A) -> Γ ⊢ (close e e') :: A

  data _i≡s_ : ∀ {n} {Γ : SEnv n} {e e' A} -> (Γ ⊢ e :: A) -> (Γ ⊢ e' :: A) -> Set where
    Iβ : ∀ {Df Darg} ->
      (IFun-E (IFun-I Df) Darg) i≡s (isubst Df Darg)

  consistent : ∀ {M} -> [] ⊢ M :: `False -> ⊥
  -- Ah. Good point; have to use a semantic model to show that.
  consistent (IFun-E D D₁) = {!!}

  open Theory {{...}}
  -- I is the initial model of the Theory
  I : Theory
  I .Tm = Syn
  I .Ty = `Type
  I .V A = Σ Syn λ e -> Σ ℕ λ n -> Σ (SEnv n) λ Γ -> Γ ⊢ e :: A
  I ._∈_ e A = Σ ℕ λ n -> Σ (SEnv n) λ Γ -> Γ ⊢ e :: A
  I .False = `False
  I .False-uninhabit M (n , Γ , D) = {!!}
  I .Base = `Base
  I .base = `base
  I .Base-I = 0 , ([] , IBase-I)
  I .var (fst , snd) = fst
  I .Var (e , n , Γ , D) = n , (Γ , D)
  I .reflect {e = e} D = (e , D)
  I .app = `app
  I .lam A f = `lam (f (`var (fromℕ 0) , 1 , (A ∷ [] , IVar (fromℕ 0) refl)))
  I .Fun = `Fun
  I .Fun-I {A = A} Df = let x = (`var (fromℕ 0) , 1 , (A ∷ [] , IVar (fromℕ 0) refl)) in
    (proj₁ (Df x)) , ((proj₁ (proj₂ (Df x))) ,
      -- This weaken in particular seems wrong; it produces weaker derivations
      -- than I intend. See test2 below.
      -- On the other hand, it needs to be weakened, since we're introduce the
      -- new variable x, which is not in the environment for the interpretation
      -- of Df.
      -- Perahps if the interpretation didn't fix an environment, but worked up
      -- to permutations of environments, this would be easier, and I wouldn't
      -- require explicit weakening rules?
      IFun-I (WeakenL (proj₂ (proj₂ (Df x)))))
  I .Fun-E (n , Γf , Df) (m , Γarg , Darg) = (m + n) , ((Γarg ++ Γf) ,
    -- (IFun-E (WeakenL Df) (WeakenR Darg)))
    IFun-E {!!} {!!})
  I ._≡lc_ (n , Γ , D1) (m , Γ' , D2) = (WeakenL D1) i≡s (WeakenR D2)
  I .Fun-β Df (m , Γarg , Da) = {!!}
  I .Fun-η = {!!}

  -- Now we compile some of our examples to Agda using this model
  module TestAgda = Test I
  test1 : [] ⊢ `base :: `Base
  test1 = (proj₂ (proj₂ TestAgda.example1))

  -- This derivation is unnecessarily weakened by the interpretation of Fun-I
  test2 : (`Base ∷ []) ⊢ (`app (`lam (`var (fromℕ 0))) `base) :: `Base
  test2 = IFun-E (proj₂ (proj₂ TestAgda.example2)) (WeakenL test1)

  strengthen : ∀ {n} {Γ : SEnv n} {A B e} ->
    (A ∷ Γ) ⊢ (shift 1 e) :: B ->
    Γ ⊢ e :: B

  strengthen-lam : ∀ {n} {Γ : SEnv n} {A B e} ->
    (A ∷ Γ) ⊢ `lam (shift 1 e) :: B ->
    Γ ⊢ `lam e :: B

  -- test2' : [] ⊢ (`app (`lam (`var (fromℕ 0))) `base) :: `Base
  -- test2' = (IFun-E (proj₂ (proj₂ TestAgda.example2)) test1)

  --test2' : [] ⊢ (`app (`lam (`var (fromℕ 0))) `base) :: `Base
  --test2' = IFun-E (IFun-I (IVar (fromℕ 0) refl)) IBase-I

  --test3 : ⊤
  ---- example4 requires the environment of the (1) free variable
  --test3 = TestAgda.example4 (tt , tt)