Sully mentioned Filinski's 1994 paper "Representing Monads" on twitter, which sent me off on a spiral of reading about delimited continuations, because I never really understood them properly.

I think I vaguely do now, mostly thanks to Ken Shan's papers, A static simulation of dynamic delimited control (which I haven't finished reading, but nicely taxonomizes four different pairs of control operators into a 2x2 square by analyzing which 'resets' they leave behind after a 'shift' fires in the operational semantics) and From shift and reset to polarized linear logic, which, and this is a surprising rarity among papers on control operators, has some completely sensible and simple typing rules early in the paper.

I have this inclination to view his
Γ // ω1 ⊢ E : τ // ω2
as a kind of lax judgment
Γ ⊢ E ÷ω2,ω1 τ
with a corresponding type operator
Γ ⊢ ◯ω2,ω1 τ
(realized as ○ω2,ω1 τ = (τ → ω1) → ω2
which is not actually a monad, but which admits a let○ rule that lets you "compose ω1,ω2 and ω2,ω3 to get ω1,ω3":
```Γ ⊢ e : ◯ω1,ω2 τ    Γ, x : τ ⊢ e' ÷ω2,ω3 τ'
------------------------------------
Γ ⊢ let ◯x = e in e' ÷ω1,ω3 τ'
```

which I can justify by noting that I can build a term of type
```((τ → ω2) → ω1)
→ (τ → (ω3 → τ') → ω2)
→ (ω3 → τ') → ω1
```

Namely the following term:
```λf : (τ → ω2) → ω1.
λg : (τ → (ω3 → τ') → ω2).
λh : (ω3 → τ').
f (λt : τ. g t (λw : ω3. h w))
```

And this business seems more "canonical" to me, whatever that means, than trying to invent the →E rule from scratch as he does, thereby baking in function-first-then-argument evaluation order.
Tags:
• #### (no subject)

Guy from Seattle team we've been working with showed up today at work; no matter how much I'm generally comfortable working with remote teams (and I…

• #### (no subject)

Didn't sleep well. Long day of work. Dinner with akiva at hanamichi.

• #### (no subject)

Sean's back in town --- good fun working with nonremote teammates.

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic