CPS in curried languages

Question

How does CPS in curried languages like lambda calculus or Ocaml even make sense? Technically, all function have one argument. So say we have a CPS version of addition in one such language:

cps-add k n m = k ((+) n m)

And we call it like

(cps-add random-continuation 1 2)

This is then the same as:

(((cps-add random-continuation) 1) 2)

I already see two calls there that aren't tail calls and in reality a complexly nested expression, the (cps-add random-continuation) returns a value, namely a function that consumes a number, and then returns a function which consumes another number and then delivers the sum of both to that random-continuation. But we can't work around this value returning by simply translating this into CPS again, because we can only give each function one argument. We need to have at least two to make room for the continuation and the 'actual' argument.

Or am I missing something completely?

Answer 1

Since you've tagged this with Haskell, I'll answer in that regard: In Haskell, the equivalent of doing a CPS transform is working in the Cont monad, which transforms a value x into a higher-order function that takes one argument and applies it to x.

So, to start with, here's 1 + 2 in regular Haskell: (1 + 2) And here it is in the continuation monad:

contAdd x y = do x' <- x
                 y' <- y
                 return $ x' + y'

...not terribly informative. To see what's going on, let's disassemble the monad. First, removing the do notation:

contAdd x y = x >>= (\x' -> y >>= (\y' -> return $ x' + y'))

The return function lifts a value into the monad, and in this case is implemented as \x k -> k x, or using an infix operator section as \x -> ($ x).

contAdd x y = x >>= (\x' -> y >>= (\y' -> ($ x' + y')))

The (>>=) operator (read "bind") chains together computations in the monad, and in this case is implemented as \m f k -> m (\x -> f x k). Changing the bind function to prefix form and substituting in the lambda, plus some renaming for clarity:

contAdd x y = (\m1 f1 k1 -> m1 (\a1 -> f1 a1 k1)) x (\x' -> (\m2 f2 k2 -> m2 (\a2 -> f2 a2 k2)) y (\y' -> ($ x' + y')))

Reducing some function applications:

contAdd x y = (\k1 -> x (\a1 -> (\x' -> (\k2 -> y (\a2 -> (\y' -> ($ x' + y')) a2 k2))) a1 k1))

contAdd x y = (\k1 -> x (\a1 -> y (\a2 -> ($ a1 + a2) k1)))

And a bit of final rearranging and renaming:

contAdd x y = \k -> x (\x' -> y (\y' -> k $ x' + y'))

In other words: The arguments to the function have been changed from numbers, into functions that take a number and return the final result of the entire expression, just as you'd expect.

Edit: A commenter points out that contAdd itself still takes two arguments in curried style. This is sensible because it doesn't use the continuation directly, but not necessary. To do otherwise, you'd need to first break the function apart between the arguments:

contAdd x = x >>= (\x' -> return (\y -> y >>= (\y' -> return $ x' + y')))

And then use it like this:

foo = do f <- contAdd (return 1)
         r <- f (return 2)
         return r

Note that this is really no different from the earlier version; it's simply packaging the result of each partial application as taking a continuation, not just the final result. Since functions are first-class values, there's no significant difference between a CPS expression holding a number vs. one holding a function.

Keep in mind that I'm writing things out in very verbose fashion here to make explicit all the steps where something is in continuation-passing style.

---

Addendum: You may notice that the final expression looks very similar to the de-sugared version of the monadic expression. This is not a coincidence, as the inward-nesting nature of monadic expressions that lets them change the structure of the computation based on previous values is closely related to continuation-passing style; in both cases, you have in some sense reified a notion of causality.

Answer 2

Short answer : of course it makes sense, you can apply a CPS-transform directly, you will only have lots of cruft because each argument will have, as you noticed, its own attached continuation

In your example, I will consider that there is a +(x,y) uncurried primitive, and that you're asking what is the translation of

let add x y = +(x,y)

(This add faithfully represent OCaml's (+) operator)

add is syntaxically equivalent to

let add = fun x -> (fun y -> +(x, y))

So you apply a CPS transform¹ and get

let add_cps = fun x kx -> kx (fun y ky -> ky +(x,y))

If you want a translated code that looks more like something you could have willingly written, you can devise a finer transformation that actually considers known-arity function as non-curried functions, and tream all parameters as a whole (as you have in non-curried languages, and as functional compilers already do for obvious performance reasons).

¹: I wrote "a CPS transform" because there is no "one true CPS translation". Different translations have been devised, producing more or less continuation-related garbage. The formal CPS translations are usually defined directly on lambda-calculus, so I suppose you're having a less formal, more hand-made CPS transform in mind.

The good properties of CPS (as a style that program respect, and not a specific transformation into this style) are that the order of evaluation is completely explicit, and that all calls are tail-calls. As long as you respect those, you're relatively free in what you can do. Handling curryfied functions specifically is thus perfectly fine.

Remark : Your (cps-add k 1 2) version can also be considered tail-recursive if you assume the compiler detect and optimize that cps-add actually always take 3 arguments, and don't build intermediate closures. That may seem far-fetched, but it's the exact same assumption we use when reasoning about tail-calls in non-CPS programs, in those languages.