Efficient compilation of code in continuation-passing style relies on two properties:
- Continuations do not escape, so we know that we do not need to allocate a closure to pass a continuation,
- Continuations return the type ⊥ (falsity), so we know that applying a continuation can be implemented as a jump.
(Source: Cong et al., Compiling with continuations, or without? whatever.)
For 1) you are relying on inlining to avoid allocating closures. However if you wanted you could still let continuations escape. Abstracted with a monadic interface, this use of CPS is inefficient but allows you to express classical control operators.
For 2) you are relying on tail calls, however if you wanted you could still modify the return value of the continuation. Abstracted with a monadic interface, this use of CPS is inefficient but would let you express delimited continuations.
For 1), a more reliable and compositional constraint is given by types of second-class (i.e. non-escaping) values, or more generally types with region, to ensure that continuations do not need to be allocated on the heap. Many higher-order functions in OCaml, including monadic binds, could benefit if OCaml understood this notion. As a naive approach, this could take the form of a generalisation of the @local attribute to arguments of functions.
For 2), a more reliable and compositional constraint is given by a primitive no-return type (or equivalently a primitive type of negation for the continuation). This could take the form of OCaml knowing to compile applications that return the empty type (type empty = |) as a jump.
Which reminds us of the equation:
programming = structure + efficiency
which I always find of great help when trying to assess papers in programming languages, especially those claiming to find programming truth in abstract mathematical structures.