August 28th, 2012

beartato phd

(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":
Γ ⊢ 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.