Denotational call-by-name semantics for untyped lambda calculus in Guarded Cubical Agda

DenSem.agda

{-# OPTIONS --cubical --guarded #-}
module DenSem where

open import Cubical.Foundations.Prelude hiding (_[_↦_])
open import Cubical.Foundations.Transport
open import Cubical.Data.Nat
open import Cubical.Data.Maybe
open import Cubical.Relation.Nullary.Base

-- Vendored Guarded Prelude (trusted code, best skipped on first read):
module Prims where
  primitive
    primLockUniv : Set₁

open Prims renaming (primLockUniv to LockU) public

private
  variable
    l : Level
    A B : Set l

postulate
  Tick : LockU

▹_ : ∀ {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

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

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

-- End of trusted code

Name = ℕ -- simpler to compare than string

decEq-ℕ : (x y : ℕ) → Dec (x ≡ y)
decEq-ℕ zero zero = yes refl
decEq-ℕ zero (suc y) = no znots
decEq-ℕ (suc y) zero = no snotz
decEq-ℕ (suc x) (suc y) with decEq-ℕ x y
... | yes p = yes (cong suc p)
... | no np = no (λ p → np (injSuc p))

instance
  decEq-ℕ-imp : {x y : ℕ} → Dec (x ≡ y)
  decEq-ℕ-imp {x} {y} = decEq-ℕ x y

data Exp : Set where
  var : Name → Exp
  lam : Name → Exp → Exp
  app : Exp → Exp → Exp

-- partial function, serving as a finite Map:
_⇀_ : ∀ {ℓ} → Set ℓ → Set ℓ → Set ℓ
A ⇀ B = A → Maybe B
infix 1 _⇀_

empty-pfun : ∀{A B : Set} → A ⇀ B
empty-pfun _ = nothing

_[_↦_] :  ∀ {A B : Set} {{dec : {x y : A} → Dec (x ≡ y)}}
          → (A ⇀ B) → A → B → (A ⇀ B)
_[_↦_] {{dec}} ρ x b y with dec {x} {y}
... | yes _ = just b
... | no  _ = ρ y

-- Finally the semantic domain model

data T (A : Set) : Set where -- Delay monad
  ret : A → T A
  step : ▹ (T A) → T A

_>>=-T_ : ∀ {A} {B} → T A → (A → T B) → T B
T.ret a >>=-T k = k a
T.step τ >>=-T k = T.step (λ α → τ α >>=-T k)

data ValueF (V⁻ : ▹ Set) : Set where
  fun : (▸ (λ α → T (V⁻ α)) → T (ValueF V⁻)) → ValueF V⁻
  stuck : ValueF V⁻

Value = fix ValueF
D = T Value

≡-D : ▸ (λ α → T (dfix ValueF α)) ≡ ▹ D
≡-D i = (@tick α : Tick) → T (pfix ValueF i α)
  -- yeah, this is what it takes unless Agda adds more support
  -- for negative guarded recursion in data types so that we can
  -- just write (▹ (T ValueF)) in the type of ValueF.fun

apply : Value → D → D
apply (ValueF.fun f) a = f (transport⁻ ≡-D (next a))
apply _              _ = T.ret ValueF.stuck

-- the meat:
D⟦_⟧_ : Exp → (Name ⇀ D) → D
D⟦ Exp.var x ⟧ ρ with ρ x
... | nothing = T.ret ValueF.stuck
... | just d  = d
D⟦ Exp.lam x e ⟧ ρ = T.ret (ValueF.fun (λ d → D⟦ e ⟧(ρ [ x ↦ T.step (transport ≡-D d) ])))
D⟦ Exp.app e₁ e₂ ⟧ ρ = (D⟦ e₁ ⟧ ρ) >>=-T (λ v → apply v (D⟦ e₂ ⟧ ρ))

idid = Exp.app (Exp.lam 0 (Exp.var 0)) (Exp.lam 0 (Exp.var 0))
omega = Exp.app (Exp.lam 0 (Exp.app (Exp.var 0) (Exp.var 0))) (Exp.lam 0 (Exp.app (Exp.var 0) (Exp.var 0)))

-- Press Ctrl-C Ctrl-N and input either res_idid or res_omega
-- to see the "normalised" expression
-- (apparently `transp v` is not considered a value, so this
-- works for omega as well)
res_idid = D⟦ idid ⟧ empty-pfun
res_omega = D⟦ omega ⟧ empty-pfun

Yes, exactly. I guess one could write pattern synonyms to get the desired API, but it would be great if Agda would just accept this definition to begin with