Explain auto continue passing style transformations

Recently I saw 3 cps transformation rules, but no explanations were given.

expressions: $$e :=x\left|e e^{\prime}\right| \lambda x \cdot e$$

rules: $$\begin{array}{l}{[[x]]=\lambda \kappa \cdot \kappa x} \\ {[[\lambda x \cdot M]]=\lambda \kappa \cdot \kappa(\lambda x \cdot[[M]])} \\ {[[M N]]=\lambda \kappa \cdot[[M]](\lambda m \cdot[[N]]](\lambda n \cdot(m n) \kappa)}\end{array}$$

When transforming fib, fib n = ... is transformed into fib n k = ..., but if we use the second rule, the first param of the transformed function will be k which differs

fib 0 = 1
fib 1 = 1
fib n = fib (n - 1) + fib (n - 2)

fib_cps 0 k = k 1
fib_cps 1 k = k 1
fib_cps n k = fib_cps (n - 1) (\x -> fib_cps (n - 2) (\y -> k (x + y)))

Could someone please explain it for me?

About the 3rd rule, why we need to transform both fn and arg when transforming function application, and why it's like this?

• Note that there are many CPS transforms. The one you posted here is the CBV (call-by-value) CPS transform. Perhaps the example you saw used another one, e.g. the CBN (call by name) CPS transform? Can you post the full code for the transformed fib? – chi Jul 16 at 11:54
• @chi I've no idea.... anyway, the full code in Haskell added. – Shuumatsu Jul 16 at 12:09

The code you posted takes a few shortcuts. The mismatch with the rules of the CPS transform comes form your code being in Haskell, which features integers (0,1,2), arithmetics (+,-), definitions by cases, and recursion, while the CPS transform only covers the pure lambda calculus, without all the bells and whistles that come with a "usual" programming language.

Anyway the idea of a CPS function is that you never return the result of the function in a direct way. Rather, you pass that result to a continuation function, usually named k, which is an additional parameter to the function. Often, it is convenient to take k as the last parameter -- this is only a convention, though, and we could choose otherwise.

For instance, the constant-zero function becomes

zero n = 0

zero_cps n k = k 0

Squaring:

square n = n*n

square_cps n k = k (n*n)

Now, in the last line I cheated a bit, since there I am using * as the regular multiplication function, instead of using a CPS variant of multiplication. Your fib_cps code does the same for + and -, which are not translated into CPS. Let's continue with this.

Now, what if we want to CPS transform this composition?

f n = square (square n)

f_cps n k = ???

Intuitively, in f_cps we want to call square_cps, take its result, and pass that to another square_cps. But we can't do that directly, since square_cps does not return its result, it passes it to the continuation. So, we need to write something like

f_cps n k = square_cps n (\m -> ...???...)

where m is the "result" of square_cps, hence m=n*n. What do we do with m? We want to square it again.

f_cps n k = square_cps n (\m -> square_cps m (\o -> ???))

here o will be the square of the square of n, hence n*n*n*n. That is the final result, so we can pass it to k, which expects the result of f.

f_cps n k = square_cps n (\m -> square_cps m (\o -> k o))

So, in CPS style, we use this "idiom":

function_cps arg1 arg2 ... arg2 (\x -> ...)

meaning "call function with the args, let x be the result, and then proceed with ...".

Code like f1 (f2 (f3 (f4 n))) becomes

f4 n  (\x4 ->
f3 x4 (\x3 ->
f2 x3 (\x2 ->
f1 x2 (\x1 ->
... use x1 here ...))))

(If you happen to be familiar with monads in Haskell, you'll see that this is very similar to a monadic do block. This is not a coincidence since CPS is strictly related to the Cont monad.)

In your fib_cps code, we need to do

fib (n-1) + fib (n-2)

This is transformed into a program which evaluates fib (n-1) first (let x be its result), then fib (n-2) second (let y be its result), and finally returns x+y. In code

fib (n-1) (\x ->
fib (n-2) (\y ->
k (x+y)))

where the last line combines the results and passes their sum to k, the continuation of the call fib_cps n k.

You might have noticed that we needed to fix an evaluation order: first fib (n-1), then fib (n-2). This order was not present in the original code. Indeed, to transform some code to CPS, we need to be more explicit about what we want to evaluate first.

In your CPS rules, application $$MN$$ is transformed into

$$[[M]](\lambda m.\ [[N]](\lambda n.\ \ldots)$$

which forces $$M$$ to be evaluated first, then $$N$$, giving an evaluation order, similarly to what happened above.

Further, the CPS term above always evaluates $$N$$. This is done according to the call-by-value (CBV) semantics, where function arguments are always evaluated. So, the CBV CPS transform matches such semantics, which is used by languages like Ocaml.

Note that Haskell, instead, uses a call-by-name (CBN) semantics instead, where e.g. zero (non terminating expression) returns 0 immediately without evaluating its argument. If we wanted to use CPS completely preserving Haskell's semantics, we should use another form of CPS called the CBN CPS transform, which is subtly different.

In your posted fib_cps code, CBV CPS is used, even in Haskell, since

1. + always evaluates its arguments
2. we are not using a CPS version of +
3. CBV CPS is arguably a bit simpler to understand

I hope this does not sound too confusing. Continuations are quite tricky to understand.

• Maybe I should use ocaml in the question description which uses CBV...You answered my question why the first param of the transformed function is k("Often, it is convenient to take k as the last parameter -- this is only a convention, though, and we could choose otherwise.") – Shuumatsu Jul 17 at 8:54
• But there is still difference, take square for example, let square_cpp k x = k (x * x) , the param of k is the result of the original function (as you said, "Rather, you pass that result to a continuation function, usually named k, which is an additional parameter to the function."). But if we transform it with the second rule, the param of k will be a lambda abstract. (I think they are both cbv cps, I don't know where I'm wrong... – Shuumatsu Jul 17 at 8:55
• @Shuumatsu In that case you would start from square = \x -> x*x and end up with square_cps2 k = k (\x k2 -> k2 (x*x)). The fib_cps style you posted avoids the top-level step and directly moves to (\x k2 -> k2 (x*x)), which is the square_cps I used above. In a sense the difference is related to considering square as something that "has no parameters and returns a lambda" or as something that "takes an argument and returns a number". In the latter case you only have a continuation function, in the former you have two. This is one of the mismatches between the transforms you posted. – chi Jul 17 at 10:17
• What do you mean by "top level step"? – Shuumatsu Jul 18 at 2:19
• I think the first form is not a standard lambda expression, am I right? so I can not directly uses only of the rules above (in this sense I can't get the two continuation functions...) And anyway, the k with param being a lambda violates the meaning that "passing result to continuation function"…thanks for your explanation. (Am I missing some prerequired knowledge? – Shuumatsu Jul 18 at 2:46