stlc-model2.agda

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ)
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
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

  Env = Vec Ty

  field
    _⊢_∈_ : {n : ℕ} -> Env n -> 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

    var : {n : ℕ} -> Fin n -> Tm

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

    Fun : Ty -> Ty -> Ty

    -- Semantic typing of open terms
    -- We're still representing lambda with "fauxAS"
    -- I don't know why. For fun?
    -- but also to consider free variable as different from local variable..
    -- more... effecty.
    -- To validate the beta/eta equations, look like I need the fauxAS argument
    -- to be closed. odd.
    Fun-I : ∀ {n} {Γ : Env n} {A f B} ->
      (∀ {x} -> ([] ⊢ x ∈ A) -> (Γ ⊢ (f x) ∈ B)) ->
      ------------------------------
      (Γ ⊢ (lam A f) ∈ (Fun A B))

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

    Base-I : ∀ {n} {Γ : Env n} ->
      -----------
      Γ ⊢ base ∈ Base

    Var : ∀ {n} {m : Fin n} {Γ : Env n} ->
      -----------
      Γ ⊢ var m ∈ (lookup Γ m)

    Weaken : ∀ {n m e A} {Γ : Env n} {Γ' : Env m} ->
      Γ ⊢ e ∈ A ->
      ----------------
      (Γ ++ Γ') ⊢ e ∈ A

    -- -- should have some equations here if I care about, you know, terms
    _≡lc_ : ∀ {n} {Γ : Env n} {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-β : ∀ {n} {Γ : Env n} {e A B} {f : Tm -> Tm} ->
      (Df : (∀ {x} -> ([] ⊢ x ∈ A) -> (Γ ⊢ (f x) ∈ B))) ->
      (Da : ([] ⊢ e ∈ A)) ->
     ---------------------------------
     (Fun-E (Fun-I Df) (Weaken {Γ = []} Da)) ≡lc (Df Da)

    Fun-η : ∀ {n} {Γ : Env n} {e A B} ->
      (Df : (Γ ⊢ e ∈ Fun A B)) ->
      ---------------------------------
      Df ≡lc (Fun-I (λ x -> (Fun-E Df (Weaken 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 -> x)) ∈ (Fun Base Base)
  example2 = Fun-I (λ x -> x)

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

  -- A free variable
  example4 : (Base ∷ []) ⊢ var (fromℕ 0) ∈ Base
  example4 = Var

-- 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

  Env = Vec STLC-Type

  G : {n : ℕ} -> Env n -> Set
  G [] = ⊤
  G (A ∷ Γ) = (El A) × (G Γ)

  γ-lookup : {n : ℕ} {Γ : Env n} -> (γ : G Γ) -> (m : Fin n) -> El (lookup Γ m)
  γ-lookup {.(ℕ.suc _)} {x ∷ Γ} (fst , _) zero = fst
  γ-lookup {.(ℕ.suc _)} {x ∷ Γ} (fst , snd) (suc m) = γ-lookup snd m

  discard : ∀ {n m} {Γ : Env n} {Γ' : Env m} -> G (Γ ++ Γ') -> G Γ
  discard {ℕ.zero} {m} {[]} {Γ'} γ = tt
  discard {ℕ.suc n} {m} {x ∷ Γ} {Γ'} (fst , snd) = fst , (discard snd)

  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
  -- the typing relation is interpreted in the reader monad for the Agda
  -- interpretation of the syntactic type.
  M ._⊢_∈_ Γ e A = (G Γ) -> El A

  M .False = STLC-False
  M .False-uninhabit _ = λ z → (z tt)

  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 = λ γ Darg → f (λ _ -> Darg) γ
  -- Function elimination applies the underlying Agda function
  M .Fun-E Df Darg γ = (Df γ) (Darg γ)

  M .var m = tt
  M .Var {n} {m} γ = γ-lookup γ m

  M .Weaken D = λ γ → D (discard γ)

  -- 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 tt

  test2 : ⊤
  test2 = TestAgda.example2 tt tt

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