Tag Info

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 ...

I think your looking for Back to Direct Style by Olivier Danvy

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 ...

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-...