guarded-stlc.agda

{-# OPTIONS --guarded #-}


open import Agda.Primitive
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym; trans)
open import Data.Unit using (⊤; tt)
open import Data.Nat -- using (ℕ; _+_; suc; _<_)
open import Data.Nat.Properties
open import Data.Fin using (Fin; fromℕ; fromℕ<)
open import Data.Vec using (Vec; lookup; []; _∷_; [_]; _++_; map)
open import Data.Product using (Σ; _,_; _×_)
open import Data.Sum using (_⊎_; inj₁; inj₂)


------------------------------------------------------------------------
-- later modality stuff copied from
-- https://github.com/agda/agda/blob/172366db528b28fb2eda03c5fc9804f2cdb1be18/test/Succeed/LaterPrims.agda
primitive
   primLockUniv : Set₁

private
  variable
    l : Level
    A B : Set l

-- We postulate Tick as it is supposed to be an abstract sort.
postulate
  Tick : primLockUniv

▹_ : ∀ {l} → Set l → Set l
▹_ A = (@tick x : Tick) -> A

▸_ : ∀ {l} → ▹ Set l → Set l
▸ A = (@tick x : Tick) → A x

next : A → ▹ A
next x _ = x

apply▹ : ▹ (A → B) → ▹ A → ▹ B
apply▹ f x a = f a (x a)

map▹ : (f : A → B) → ▹ A → ▹ B
map▹ f x α = f (x α)

postulate
  dfix : ∀ {l} {A : Set l} → (▹ A → A) → ▹ A
  pfix : ∀ {l} {A : Set l} (f : ▹ A → A) → dfix f ≡ (\ _ → f (dfix f))

--pfix' : ∀ {l} {A : Set l} (f : ▹ A → A) → ▸ \ α → dfix f α ≡ f (dfix f)
--pfix' f α i = pfix f i α

fix : ∀ {l} {A : Set l} → (▹ A → A) → A
fix f = f (dfix f)

------------------------------------------------------------------------
-- STLC + Fix

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

Env : ℕ -> Set
Env n = Vec Type n

Var : ∀ {n} -> Env n -> Type -> Set
Var {n} Γ A = Σ (Fin n) λ m -> (lookup Γ m) ≡ A

data STLC : ∀ {n} -> (Env n) -> Type -> Set where
  var : ∀ {n} {Γ : Env n} {A} ->
    Var Γ A ->
    STLC Γ A
  nlit : ∀ {n} {Γ : Env n} ->
    ℕ ->
    STLC Γ `Nat
  lam : ∀ {n} {Γ : Env n} {A B}  ->
    (STLC (A ∷ Γ) B) ->
    STLC Γ (`Fun A B)
  app : ∀ {n} {Γ : Env n} {A B}  ->
    (STLC Γ (`Fun A B)) -> STLC Γ A ->
    STLC Γ B
  rec : ∀ {n} {Γ : Env n} {A} ->
    (STLC (A ∷ Γ) A) ->
    STLC Γ A

module examples where
  eg0 : ∀ {n} {Γ : Env n} -> STLC Γ `Nat
  eg0 = nlit 0


  eg1 : ∀ {n} {Γ : Env n} -> STLC Γ (`Fun `Nat `Nat)
  eg1 = lam (var ((fromℕ< {0} 0<1+n) , refl))


  eg2 : ∀ {n} {Γ : Env n} -> STLC Γ `Nat
  eg2 = app (lam (var ((fromℕ< {0} 0<1+n) , refl))) (nlit 5)

  eg3 : ∀ {n} {Γ : Env n} -> STLC Γ `Nat
  --_ = app (rec {`Fun `Nat `Nat} (λ _ f -> (lam (λ x -> (app (var f) (var x)))))) (nlit 0)
  eg3 = app (rec {A = `Fun `Nat `Nat}
               (lam (app (var ((fromℕ< {1} (s<s z<s)) , refl)) (var ((fromℕ< {0} z<s) , refl)))))
      (nlit 0)

  eg4 : ∀ {n} {Γ : Env n} -> STLC Γ `Nat
  eg4 = app (rec {A = `Fun `Nat `Nat} (lam (var ((fromℕ< {0} z<s) , refl)))) (nlit 0)


-- This L-algebra comes from page ~36 https://mpaviotti.github.io/assets/papers/paviotti-phdthesis.pdf
L : Set -> Set
L A = fix λ X -> A ⊎ ▸ X

-- the left injection, which is trivial
η : ∀ {A} -> A -> L A
η = inj₁

-- the right injection, with casts
θ : ∀ {A} -> ▹ L A -> L A
θ {A} x = inj₂ (subst ▸_ (sym (pfix (λ X → A ⊎ (▸ X)))) x)

Value : Type -> Set
Value `Nat = L ℕ -- to add fix, base values become L-algebras?
Value (`Fun A B) = (Value A -> Value B)

open import Data.Empty using (⊥)

δ : ∀ {A} -> L A -> L A
δ {A} x = θ (next x)

-- the abuse of notation in the paper calls this θ, too.
synθ : ∀ {B} -> ▹ (Value B) -> (Value B)
synθ {`Nat} = θ
synθ {`Fun A B} = λ f -> λ x -> (synθ (apply▹ f (next x)))

pointwise : ∀ {n} -> (Γ : Env n) -> (Type -> Set) -> Set
pointwise {.zero} [] f = ⊤
pointwise {.(suc _)} (A ∷ Γ) f = (f A) × (pointwise Γ f)

env-ref : ∀ {n} {Γ : Env n} {f} {A} -> (γ : pointwise Γ f) -> {m : Fin n} -> (p : lookup Γ m ≡ A) -> f A
env-ref {Γ = x ∷ Γ} (fst , snd) {Fin.zero} refl = fst
env-ref {Γ = x ∷ Γ} (fst , snd) {Fin.suc m} refl = (env-ref snd refl)

eval : ∀ {n} {Γ : Env n} {A} -> STLC Γ A -> (γ : (pointwise Γ (λ A -> Value A))) -> (Value A)
eval (var (fst , snd)) γ = env-ref γ snd
eval (nlit x) γ = inj₁ x
eval (lam f) γ = λ x → (eval f (x , γ))
eval (app f rand) γ = (eval f γ) (eval rand γ)
-- the only clever bit is now what happens with rec.
-- had to uncurry a bit of the thesis
eval {A = A} (rec e) γ = fix λ x -> (synθ {A} (apply▹ (next (λ y -> (eval e (y , γ)))) x))

-- eg0 terminates at 0
_ : (eval examples.eg0) tt ≡ (inj₁ 0)
_ = refl

-- eg2 terminates at 5
_ : (eval examples.eg2) tt ≡ (inj₁ 5)
_ = refl

-- eg3.. doesn't terminate
-- Not really sure what the normal form of a non-terminating computation looks like...
-- would guess δ followed by... something
_ : (eval examples.eg3) tt ≡ (θ (fix λ f -> {!!}))
_ rewrite (pfix (λ X -> ℕ ⊎ (▸ X))) = {!!}

-- eg4, terminates, but through recursion, after one step of computation.
-- delta represents one step.
_ : (eval examples.eg4) tt ≡ (δ (η 0))
_ rewrite (pfix (λ X -> ℕ ⊎ (▸ X))) = refl