Optional Section: The CPS Transformation in OCaml

The CPS transformation reorganizes a computation is such a way that every function application is in tail-form (not nested in the argument to another function call). This is done by converting every expression into a function which accepts a parameter, the continuation. In addition, every function is rewritten to accept an additional parameter. The continuation accepts a single value, the result of the partial computation, and encodes what work still needs to be done. At the top level, the identity continuation λx.x, is passed in, indicating that no work remains to be done.

Converting programs to CPS allows us to more easily model control flow constructs such as goto.

Recall the syntax for LC: e = i | x | λx.e | e1 e2. We can express the CPS transformation over LC as follows. The notation [[e]] means to perform the CPS transformation on e.

    [[i]] -> λk . k i
    [[x]] -> λk . k x
 [[λx.e]] -> λk . k λk' . λx . [[e]] k'
[[e1 e2]] -> λk . [[e1]] λf . ([[e2]] λx . f k x)

The transformation for values simply rewrites them as functions accepting a continuation and applying it to a value. Additionally, the transformation for λx.e adds a parameter k', the additional continuation accepted by the function.

Function application is an interesting case, however. Note that, the way CPS is defined, the value of the expression wrapped by a continuation (ie the partial result of the subexpression) is passed as the first parameter to the continuation. That is, to get the value of the function that needs to be applied (f), pass λf.... as the continuation for [[e1]]. Similarly, pass λx.... as the continuation for [[e2]]. Finally, pass k in to the application of f to x as the additional parameter.

The CPS transformation for LC can be coded in O'Caml as follows. The cpsIt actually performs the transformation; the cps function applies the CPS-rewritten expression to the identity continuation, λtop.top.

let rec cpsIt e =
  let k = gensym "k" in
    match e with
        Con i ->
          Lam (k, App (Var k, Con i))
      | Var n ->
          Lam (k, App (Var k, Var n))
      | Lam (x,e) ->
          let k' = gensym "k'" in
          Lam (k,App (Var k,
                  (Lam (k',Lam (x,App (cpsIt e, Var k'))))))
      | App (e1,e2) ->
          let f = gensym "f" in
          let x = gensym "x" in
          Lam (k,App (cpsIt e1, Lam (f,
                 App (cpsIt e2,  Lam (x,
                 App (App (Var f, Var k), Var x))))))

let cps e = App((cpsIt e), Lam ("top",Var "top"))

CPSing the CPS Transformation

We can take this version of the CPS transformation and effectively CPS it. This makes the code somewhat shorter and also makes the resulting code somewhat more compact.

let rec cpsIt e k =
  match e with
    Con i ->
      k e
  | Var n ->
      k e
  | Lam (x,e) ->
      let y = gensym "k" in
      k (Lam (y, Lam (x,(cpsIt e (fun r -> App (Var y, (r)))))))
  | App (e1,e2) ->
      cpsIt e1 (fun f ->
      cpsIt e2 (fun x ->
      let y = gensym "m" in
      App(App(f,(Lam(y,(k(Var y))))),x)))

Again, the cpsIt function performs the actual CPS transformation. The cps function applies the results of the CPS transformation to the identity continuation. It also passes what is effectively the identity meta-continuation (the application of the identity object-continuation to the parameter) into the CPS transformation.

let cps e =
  let a = gensym "a" in
  let b = gensym "b" in
  (App (Lam (a,cpsIt (exp e) (fun c -> App(Var a,(c)))), Lam (b,Var b)))

Back to course website