Question

I'm reading Dijkstra Monads for Free for a presentation I'll be doing and it's pretty meaty. One of the things that I keep running into is the term "CPS'ing". I've read a little bit on continuation-passing style (i.e., I've read through most of the Wikipedia page and it didn't feel like utter nonsense...) but I'm still not clear what the phrase "CPS'ing" means.

They give an example, which I will duplicate here, after which I will present the main pattern I see:

Rather than being given manually, we show that these predicate transformers can be automatically derived by CPS'ing purely functional definitions of monadic effects (with answer type Type). For instance, rather than defining WP_ST, one can simply compute it by CPS'ing the familiar ST monad (i.e., state -> a * state), deriving

WP_ST a = ((a * state) -> Type) -> state -> Type

(For context, this can be found on page 1, first full paragraph at the top of the second column).

So there is a pretty obvious pattern here: Given some type

a1 -> a2 -> ... -> an

we can map it via the contraviariant functor F (a -> b) = (b -> a) that just reverses the arrows, yielding

an -> ... -> a2 -> a1

and then replacing each ai with (ai -> Type).

Is this a reasonable interpretation of the term "CPS'ing"? Also, it's not clear to me why this is useful - is there any motivation for what is gained by applying such a transformation?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top