Semantics of a weak delay modality

In my previous post, I sketched some typing rules for a guarded recursion calculus. Now I'll give its categorical semantics. So, suppose we have a Cartesian closed category with a delay functor and the functorial action and natural transformations:

•(f : A → B)  : •A → •B
δ             : A → •A
ι             : •A × •B → •(A × B)
ι⁻¹           : •(A × B) → •A × •B
fix           : (•A ⇒ A) → A

I intend that the next modality is a Cartesian functor (ie, distributes through products) and furthermore we have a delay operator δ. We also have a fixed point operator for the language. However, I don't assume that the delay distributes through the exponential. Now, we can follow the usual pattern of categorical logic, and interpret contexts and types as objects, and terms as morphisms. So types are interpreted as follows:

〚A → B〛 = 〚A〛 ⇒ 〚B〛
〚•A〛    = •〚A〛

Note that we haven't done anything with time indices yet. They will start to appear with the interpretation of contexts, which is relativized by time:

〚·〛ⁿ         = 1
〚Γ, x:A[j]〛ⁿ = 〚Γ〛 × •⁽ʲ⁻ⁿ⁾〚A〛  if j > n
〚Γ, x:A[j]〛ⁿ = 〚Γ〛 × 〚A〛       if j ≤ n

The idea is that we interpret a context at time n, and so all the indices are interpreted relative to that. If the index j is bigger than n, then we delay the hypothesis, and otherwise we don't. Then we can interpret morphisms at time n as 〚Γ ⊢ e : A[n]〛 ∈ 〚Γ〛ⁿ → 〚A〛, which we give below:

〚Γ ⊢ e : A[n]〛 ∈ 〚Γ〛ⁿ → 〚A〛

〚Γ ⊢ μx.e : A[n]〛              = 
    fix ○ λ(〚Γ, x:A[n+1] ⊢ e : A[n]〛)

〚Γ ⊢ x : A[n]〛                 = 
    π(x)    (where x:A[j] ∈ Γ)

〚Γ ⊢ λx.e : A → B[n]〛          = 
    λ(〚Γ, x:A[n] ⊢ e : B[n]〛)

〚Γ ⊢ e e' : B[n]〛              = 
    eval ○ ⟨〚Γ ⊢ e : A → B[n]〛, 〚Γ ⊢ e' : B[n]〛⟩

〚Γ ⊢ •e : •A[n]〛               = 
    •〚Γ ⊢ e : A[n+1]〛 ○ Nextⁿ(Γ)

〚Γ ⊢ let •x = e in e' : •B[n]〛 = 
    〚Γ, x:A[n+1] ⊢ e' : B[n]〛 ○ ⟨id(Γ), 〚Γ ⊢ e : •A[n]〛⟩

Most of these rules are standard, with the exception of the introduction rule for delays. We interpret the body •e at time n+1, and then use the functorial action to get an element of type •A. This means we need to take a context at time n and produce a delayed one interpreted at time n+1.

Nextⁿ(Γ) ∈ 〚Γ〛ⁿ → •〚Γ〛ⁿ⁺¹
Nextⁿ(·)         = δ₁
Nextⁿ(Γ, x:A[j]) = ι ○ (Nextⁿ(Γ) × δʲ⁻ⁿ)  if j > n
Nextⁿ(Γ, x:A[j]) = ι ○ (Nextⁿ(Γ) × δ)     if j ≤ n

I think this is a pretty slick way of interpreting hybrid annotations, and a trick worth remembering for other type constructors that don't necessarily play nicely with implications.

Next up, if I find a proof small enough to blog, is a cut-elimination/normalization proof for this calculus.