I just learned today that in classical linear logic, the following type isomorphism holds: $$ (!A \multimap R) \multimap R \qquad\simeq\qquad R^\bot \multimap (!A \otimes R^\bot) $$
So linear CPS and linear state are the same thing, up to a dual notion of observation, and this is the fundamental reason why SSA and CPS are equivalent program representations.
Apparently, this is the observation that prompted Egger, Møgelberg and Simpson to invent the enriched effect calculus, which is a reformulation of Paul Levy's call-by-push-value to make the linear nature of control more apparent. I guess this is also why Møgelberg and Staton were able to prove that linear state is a universal effect.
Now I'm curious how all this fits with the story of the algebraic theory of effects, such as Pretnar and Plotkin's effect handlers.
that made me think of how you can rework "s -> (a,s)" into "forall o. (a -> s -> o) -> s -> o" in haskell to gain performance for some uses of the state monad (losing some lazyness though).
ReplyDeleteThere's a package on hackage about these transformations for other monads btw, based on right kan extensions:
http://hackage.haskell.org/package/monad-ran