Hello,

As Bob Harper is fond to say, functions in HOAS are pure and total, so CPS transformation brings nothing new. A long time ago, in "CPS Transformation after Strictness Analysis" (LOPLAS 1993) and in "On the Transformation between Direct and Continuation Semantics" (MFPS 1993), John Hatcliff and I elaborated on this idea by constructing mixed CPS transformations that depended on the lambda-abstractions and applications in the source program being strict / non-strict, or total/ non-total. For example, a total function would be left in direct style, while a non-total function would be CPS-transformed. So a program where all functions are total would be mapped to itself, while a program where all functions are not total would be completely CPS-transformed. A mixed program where some functions are total (eg, because they implement HOAS) and others are not would be transformed into a program where not all functions are in CPS, but others remain in direct style.

So now you know why

fn f => (f 10) + (f 20)

is CPS-transformed into

fn k => k (fn f => fn k =>
f 10 (fn v1 =>
f 20 (fn v2 =>
k (v1 + v2))))

instead of into

fn k => k (fn f => fn k =>
f 10 (fn v1 =>
f 20 (fn v2 =>
plus_c (v1, v2) k)))

where plus_c is the CPS version of +.

The reason is that (ignoring integer overflow) + is total, and therefore can be left in direct style in the residual CPS program without endangering Plotkin's Indifference theorem.

The point is elaborated further in Lasse Nielsen's BRICS Research Report "A Selective CPS Transformation" at

http://www.brics.dk/RS/01/Abs/BRICS-RS-01-Abs/BRICS-RS-01-Abs.html#BRICS-RS-01-30(and while you are at it, you can also peek at BRICS RS 01-29, "A Unifying Approach to Goal-Directed Evaluation", which is fun).

Best,

-- Olivier Danvy