I am struggling to wrap my head around this compiler technique, so let's say here's my `factorial` function `def factorial(value: int) -> int: if value == 0: return 1 else: return factorial(value-1) * value ` It is recursive, but not TCO friendly yet, so, as the theory goes, the first thing to try here is translate it to CPS: `def factorial_cont(value: int, cont: typing.Callable[[int], T]) -> T: if value == 0: return cont(1) else: return factorial_cont(value-1, lambda result: cont(value * result)) ` Now, as the function is tail call recursive, I can do the usual trick with the while loop: `def factorial_while(value: int, cont: typing.Callable[[int], T]) -> T: current_cont = cont current_value = value while True: if current_value == 0: return current_cont(1) else: current_cont = lambda result: current_cont(current_value * result) # note: in actual python that would look like # current_cont = lambda result, c=current_cont, v=current_value: c(v * result) current_value = current_value - 1 ` This `current_cont` thing effectively becomes a huge composition chain, in `haskell` terms for the `value == 3` that would be `let resulting_cont = ((initial_cont . (3*)) . (2*)) . (1*)`, where `initial_cont` is safe to default to `id`, and surely enough `resulting_cont value == value!`. But I also know the trick with "`accumulator`" value: `def factorial_acc(value: int, acc: int = 1) -> int: current_acc = acc current_value = value while True: if current_value == 1: return current_acc else: current_acc = current_acc * current_value current_value = current_value - 1 ` which looks pretty much identical to the CPS version after the introduction of while loop. The question is, how exactly do I massage the continuation `let resulting_cont = ((initial_cont . (3*)) . (2*)) . (1*)` into t

Recently I saw 3 cps transformation rules, but no explanations were given. expressions: $e :=x\left|e e^{\prime}\right| \lambda x \cdot e$ rules: $$ \begin{array}{l}{[[x]]=\lambda \kappa \cdot \kappa x} \\ {[[\lambda x \cdot M]]=\lambda \kappa \cdot \kappa(\lambda x \cdot[[M]])} \\ {[[M N]]=\lambda \kappa \cdot[[M]](\lambda m \cdot[[N]]](\lambda n \cdot(m n) \kappa)}\end{array} $$ When transforming `fib`, `fib n = ...` is transformed into `fib n k = ...`, but if we use the second rule, the first param of the transformed function will be `k` which differs ``` fib 0 = 1 fib 1 = 1 fib n = fib (n - 1) + fib (n - 2) fib_cps 0 k = k 1 fib_cps 1 k = k 1 fib_cps n k = fib_cps (n - 1) (\x -> fib_cps (n - 2) (\y -> k (x + y))) ``` Could someone please explain it for me? About the 3rd rule, why we need to transform both fn and arg when transforming function application, and why it's like this?

Let's call the two languages in question (untyped lambda calculus with single or multiple prompt delimited continuations) L_delim and L_prompt. Is it possible to express multi-prompt delimited continuations in terms of single-prompt delimited continuations By express I mean the macro-expressible sense (to provide some kind of translation that doesn't involve interpreter overhead), of course it's possible to write an interpreter for multi-prompt delimited continuations even in pure lambda calculus. I expected a negative result for this, that it's not possible but I don't know how that would be shown. Thanks for any input on this.

I'm reading Dijkstra Monads for Free for a presentation I'll be doing and it's pretty meaty. One of the things that I keep running into is the term "CPS'ing". I've read a little bit on continuation-passing style (i.e., I've read through most of the Wikipedia page and it didn't feel like utter nonsense...) but I'm still not clear what the phrase "CPS'ing" means. They give an example, which I will duplicate here, after which I will present the main pattern I see: Rather than being given manually, we show that these predicate transformers can be automatically derived by CPS'ing purely functional definitions of monadic effects (with answer type `Type`). For instance, rather than defining `WP_ST`, one can simply compute it by CPS'ing the familiar `ST` monad (i.e., `state -> a * state`), deriving ``` WP_ST a = ((a * state) -> Type) -> state -> Type ``` (For context, this can be found on page 1, first full paragraph at the top of the second column). So there is a pretty obvious pattern here: Given some type ``` a1 -> a2 -> ... -> an ``` we can map it via the contraviariant functor `F (a -> b) = (b -> a)` that just reverses the arrows, yielding ``` an -> ... -> a2 -> a1 ``` and then replacing each `ai` with `(ai -> Type)`. Is this a reasonable interpretation of the term "CPS'ing"? Also, it's not clear to me why this is useful - is there any motivation for what is gained by applying such a transformation?

According to the Wikipedia page on static-single assignment (SSA), SSA is used by large and well-known projects such as LLVM, GCC, MSVC, Mono, Dalvik, SpiderMonkey, and V8 while the page on projects using continuation-passing style (CPS) is a bit lacking in comparison. I have this notion that CPS is preferred by compilers and interpreters that implement primarily functional languages -- particularly, Haskell and Scheme seem to have strong inclinations towards CPS style due to the restrictions on mutation or need for first-class continuation support (I would guess that Smalltalk would possibly need this as well). The major literature that I've encountered that uses CPS seems to be those that are primarily working on Scheme or are related to Scheme in some respect. Is there any particular reason why SSA is used in industry besides momentum of adoption? SSA and CPS have a close relationship; that means that it would be easy to state either in terms of another, but perhaps the information representation would be less compact or less efficient for CPS.

I'm looking into implementation techniques for programming languages, and recently came across spaghetti stacks, which are supposedly a good fit for a continuation passing style model (given their use in e.g. Scheme and SML/NJ). For sake of simplicitly, let's only consider a single-threaded processes for this question. However, I'm a bit confused by the diagram on Wikipedia (also found elsewhere). In particular, I don't understand how such a situation can arise. I can only imagine that the grayed-out branches are unreachable and should be garbage-collected. On the other hand, with my vague understanding of how to implement CPS using spaghetti stacks, I can't imagine how you could ever get a loop in that structure. I have to conclude that, rather than a "parent-pointer tree", it's actually a directed acyclic graph, with as many non-garbage sources as there are threads, and as many sinks as there are (potential) "exit points". But my understanding of this implementation is pretty vague, so I guess I'm probably missing something. I hope someone can enlighten me here on "spaghetti call stacks", by which I mean the data structure as used in Scheme and/or SML/NJ to implement CPS-based processes. - Given the following spaghetti call stack: ``` [exit point] <-- ... <-- [frame A] <-- [frame B (active)] ^ `---- [frame C] ``` As far as I understand, any flow control from B either unwinds the stack by jumping to a parent (A becomes active, unreachable B is now garbage), or replacing the active frame by a subgraph, connected only using references held by B or references to the new frames. Execution can't flow to frame C, which must mean that frame C is garbage. - Rather than the previous situation, I'd think that the following garbage-free situation may arise: ``` [exit point] <-- ... <-- [frame W] <-- [frame X] <-- [frame Z (active)] ^ |

Using continuation passing style, many common language constructs can be written in a simple language with recursion, including loops (using trampolining), exceptions, generators and even function returns. I have found numerous examples of other language constructs, but all examples I have seen use if-statements directly. Noting the power of CPS, I got curious: Can one write an if-statement in CPS without using an if-statement directly? The naive attempt would be something along these lines: ``` if_cps(condition, true_body, false_body, current_continuation) { if(condition) true_body(current_continuation); else false_body(current_continuation); } ``` but obviously this is a failure, since I used an if-statement directly.

I am reading the paper Compiling with Continuations, Continued, and in section 2.4, Comparison with ANF, the author draws attention to the fact that ANF is not closed under beta reduction. The snippet of text in question follows: As Flanagan et al. (1993) suggest, the “back end of an A-normal form compiler can employ the same code generation techniques that a CPS compiler uses”. However, as we mentioned in the Introduction, it is not so apparent whether ANF is ideally suited to optimization. After all, it is not even closed under the usual rule for β reduction (λx.A) v → A[v/x]. What does the author mean by this last sentence? (My guess is that he means ANF beta reduction can introduce new, unbound variables into the reduced term. If that is the case, I am having a hard time visualizing when this would occur and would appreciate outside confirmation that my interpretation is correct.)

I've been using Clojure for about 18 months. Recently, I've come across terms such as Monads, Continuations, et al which I'd like to learn about. I could visit Wikipedia and read about these two topics, but I'm looking for a reference which also help me learn about related matters that I don't even know exist. Is there a book on this particular topic (if it even qualifies as one)? Would I pick these things up by learning about type systems or language design in general? Should I just learn Haskell to get exposure?

The yin yang puzzle was written in Scheme. Since it uses call/cc, it is not possible to express it in a pure lambda expression, unless we do a CPS transform. However, given the fact that $\lambda \mu$-calculus have the power to model call/cc, is it possible to write an equivalent $\lambda \mu$-expression? I am still learning $\lambda \mu$-deductions, so this would be a good example to show how the deduction works. There is no need to model the "display" command in a pure expression. Ideally only showing how the calculus keep looping and evaluates diffident terms again and again. UPDATE My translation in $\lambda$-expression with CPS: ``` (λcallcc.callcc (λyin.callcc (λyang.yin yang))(λcc.cc cc) ``` In CPS, `(λcc.cc cc)` is what "call with current continuation" means. So the expression takes it as a parameter. This will result in assign the sub-expression starts `λyin` assign its continuation into parameter `yin`. And then in the body, the second callcc assigns the `yang` of sub-expression starts `λyang` into itself. Finally, apply `yin yang`. Note the above translate is not full CPS, only the concept of call/cc has been translated. But it provides the same behavior and it is not hard to do a full CPS translate.