[antonvs]

Yes. Check out the book "Compiling with Continuations" by Andrew Appel.

Not only can a compiler "convert direct style to CPS under the hood," it's one of the more efficient and effective ways to implement a compiler.

At a high level, CPS provides an intermediate form that's well suited to transformation into machine-oriented forms like machine code and bytecode, but is still high-level enough to be able to support both human and automated reasoning.

Also see the paper, "A Correspondence between Continuation Passing Style and Static Single Assignment Form"[1] which describes the equivalence between SSA, commonly used in imperative language compilers, and CPS.

This is one of the many cases where a well-motivated functional solution turns out to be one of the better solutions to a problem, to the point that a version of it is used even in imperative contexts.

[1] https://www.cs.purdue.edu/homes/suresh/502-Fall2008/papers/k...

[hencq]

In addition to those, Matt Might has an article that breaks down the steps as well: http://matt.might.net/articles/cps-conversion/

[milani]

Cool, I'll check them out. If it is "one of the more efficient and effective ways to implement a compiler", are we aware of any non-functional languages that use this style in their compilers? Asking since most compilers use LLVM and LLVM is in SSA form.

[antonvs]

The insight in the Kelsey paper I linked is that SSA and CPS are essentially equivalent. SSA is more or less CPS expressed at a kind of lower level, more like a bytecode. So one answer to the question is that all SSA compilers are already using a form of CPS.

If you wanted to use traditional CPS explicitly, you'd need a transformation step that converts the imperative source code into a more functional intermediate form so that it can be CPS'd. There might be benefits to that, since CPS can be easier to analyze than SSA. But I'm not aware of any real imperative compilers that do it.

There's been academic work on it, like: https://arxiv.org/abs/1202.3247

One of the potential benefits is covered in that paper: the ability to prove correctness of the transformations. That kind of thing is easier to do given the mathematical tractability of CPS, due to its connection to lambda calculus.