cubical-phoas-stlc.agda

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical

cong : ∀ {ℓ} {A : Set ℓ} {x y : A} {B : A → Set ℓ} (f : (a : A) → B a) (p : x ≡ y)
       → PathP (λ i → B (p i)) (f x) (f y)
cong f p i = f (p i)

open import Data.Nat
open import Data.Nat.Properties
open import Data.Fin
open import Relation.Nullary
open import Data.Bool

data Type : Set where
  `Nat : Type
  `Fun : Type -> Type -> Type

Value : Type -> Set
Value `Nat = ℕ
Value (`Fun A B) = Value A -> Value B

-- a little weird STLC model that only binds semantics values and not syntactic
-- values.
-- a stepping stone toward PHOAS
module STLC-ind where
  data STLC : Type -> Set₁ where
    var : ∀ {A} -> Value A -> STLC A
    nlit : ℕ -> STLC `Nat
    lam : ∀ {A B}  ->
      (Value A -> STLC B) ->
      STLC (`Fun A B)
    app : ∀ {A B}  ->
      (STLC (`Fun A B)) -> STLC  A ->
      STLC B

  module examples where
    _ : STLC `Nat
    _ = nlit 0


    _ : STLC (`Fun `Nat `Nat)
    _ = lam (λ x -> var x)


    _ : STLC `Nat
    _ = app (lam (λ x -> var x)) (nlit 5)

-- a little weird HIT version of STLC, where β is baked in.
module STLC-HIT where
  mutual
    data STLC : Type -> Set where
      var : ∀ {A} -> (Value A) -> STLC A
      nlit : ℕ -> STLC `Nat
      lam : ∀ {A B}  ->
        (Value A -> STLC B) ->
        STLC (`Fun A B)
      app : ∀ {A B}  ->
        (STLC (`Fun A B)) -> STLC A ->
        STLC B
      β : ∀ {A B} {f : Value A -> STLC B} {e} ->
        (app (lam f) e) ≡ (f (eval e))

    eval : ∀ {A} -> STLC A -> (Value A)
    eval (var e) = e
    eval (nlit x) = x
    eval (lam e) = (λ a -> (eval (e a)))
    eval (app e1 e2) = (eval e1) (eval e2)
    eval (β {f = f} {e = e} i) = (eval (f (eval e)))

    reflect : ∀ {A} -> Value A -> STLC A
    reflect {`Nat} v = nlit v
    reflect {`Fun A B} v = lam λ x → (reflect (v x))

    normalize : ∀ {A} -> STLC A -> STLC A
    normalize {A} e = (reflect (eval e))

  -- huzzah I have my equational theory over my syntax from NbE.
  -- The NbE only comes because I used semantic binding...
  -- lets try binding syntax next
  _ : (normalize (app (lam var) (nlit 5))) ≡ (nlit 5)
  _ = cong normalize (β {f = var} {e = nlit 5})


module cubical-phoas where
  -- uh oh. Moving Var to an index bumps up the universe level... that's going
  -- to cause problems
  data STLC : {Var : Type -> Set} -> Type -> Set₁ where
    var : ∀ {A Var} -> (Var A) -> STLC {Var} A
    nlit : ∀ {Var} -> ℕ -> STLC {Var} `Nat
    lam : ∀ {Var A B}  ->
      (Var A -> STLC {Var} B) ->
      STLC {Var} (`Fun A B)
    app : ∀ {Var A B}  ->
      (STLC {Var} (`Fun A B)) -> STLC {Var} A ->
      STLC {Var} B
    -- This is certainly wrong.
    -- I need to instantiate app's var to STLC {Var}.
    -- The left side will have type STLC {STLC {Var}} but the right side has
    -- type STLC {Var}.
    -- it only appears to work if I leave the implicits unsolved
    β : ∀ {Var f e} ->
      (app (lam f) e) ≡ (f e)

  _ : app (lam var) (nlit 5) ≡ (nlit 5)
  _ = β