patternMinor
Continuation-passing style: what is meant by "CPS'ing"?
Viewed 0 times
meantcontinuationwhatcpsingpassingstyle
Problem
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
(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
we can map it via the contraviariant functor
and then replacing each
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?
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), derivingWP_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 -> ... -> anwe can map it via the contraviariant functor
F (a -> b) = (b -> a) that just reverses the arrows, yieldingan -> ... -> a2 -> a1and 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?
Solution
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.
$$
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.
Context
StackExchange Computer Science Q#84503, answer score: 3
Revisions (0)
No revisions yet.