7
The closest I've seen to an answer to this question is the first picture in the Gallery of Doctor Melliès,
illustrating the map
$$\neg\neg A \otimes \neg\neg B \longrightarrow \neg\neg(A \otimes B)$$
which exists in any dialogue category (i.e., a monoidal category with closures into a fixed object). Note that the left-to-right CPS transform of general ...
5
I think your looking for Back to Direct Style by Olivier Danvy
4
Augmenting Noam's answer:
Removing the implicit currying, $f : A \to B \to C$ is the same thing as $uncurry( f) : A \times B \to C$. Strong monads $T$ give a map (two, actually!): $dblstr : T A \times T B \to T (A\times B)$.
We therefore have a map:
$ T A \times T B \xrightarrow {dblstr} T(A\times B) \xrightarrow{uncurry(f)} TC $
If we instantiate this ...
3
One possible answer would be: apply your CPS style program to the identity continuation, and perform symbolic evaluation of every $\beta$-redex. This should give a reasonable "direct-style" interpretation of your program, if there was not much $\lambda$-lifting (turning nameless functions into named top-level functions).
Note that this works for side-effect-...
Only top voted, non community-wiki answers of a minimum length are eligible
Related Tags
continuations × 2cps-transforms × 2
pl.programming-languages × 1
functional-programming × 1
monad × 1