(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 ÷ω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":
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) → ω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.
