### (no subject)

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 ÷

with a corresponding type operator

Γ ⊢ ◯

(realized as ○

which is not

which I can justify by noting that I can build a term of type

Namely the following term:

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.

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) → ω2which 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 = eine' ÷_{ω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.