Continuation-passing style: what is meant by "CPS'ing"?

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?

Answer 1

I had only a quick look at the paper, but I believe that they are referring to moving from $$ t_1 \to t_2 \cdots \to t_n $$ to $$ t_1 \to t_2 \cdots \to \lnot \lnot t_n $$ where $\lnot t = (t \to r)$ for some fixed return type $r$. In the paper, they choose $r = \sf Type$. So, we get $$ t_1 \to t_2 \cdots \to (t_n \to {\sf Type}) \to {\sf Type} $$ In the case of the state monad we get $$ state \to ((a \times state) \to {\sf Type}) \to {\sf Type} $$ which is isomorphic to (exchanging the order of the arguments) $$ ((a \times state) \to {\sf Type}) \to state \to {\sf Type} $$

Anyway, Sect. 2.3 of the paper shows the actual transform.