<p>The closest I've seen to an answer to this question is the first picture in <a href="http://www.pps.univ-paris-diderot.fr/~mellies/gallery.html" rel="noreferrer">the Gallery of Doctor Melliès</a>,
<img src="https://i.sstatic.net/lqhD9.jpg" alt="~~A * ~~B |- ~~(A * B)">
illustrating the map
$$\neg\neg A \otimes \neg\neg B \longrightarrow \neg\neg(A \otimes B)$$
which exists in any <em>dialogue category</em> (i.e., a monoidal category with closures into a fixed object).  Note that the left-to-right CPS transform of general binary functions reduces to applying this map and then composing with the functorial action of the double-negation monad.</p>

<p>The illustration basically follows the standard conventions of <a href="http://ncatlab.org/nlab/show/string+diagram" rel="noreferrer">string diagrams</a> (modulo the polarizations of the wires, which are meant to indicate the flow of control).  In particular, the map is constructed in three steps: twice applying the <a href="http://ncatlab.org/nlab/show/tensorial+strength" rel="noreferrer">strength</a> ($\kappa\wedge$) of the monad induced from the negation self-adjunction, and then applying the counit of the adjunction ($\epsilon$).  At this level of abstraction, the derivation is generic for any adjunction giving rise to a strong monad, and you could then ask for a more abstract characterization of such adjunctions, which Melliès has also <a href="http://www.pps.univ-paris-diderot.fr/~mellies/tensorial-logic/8-parametric-monads-and-enriched-adjunctions.pdf" rel="noreferrer">written about</a>.</p>

CC BY-SA 3.0
2013-12-28T13:57:23.877Z
2013-12-28T13:57:23.877Z
Noam Zeilberger
<p>Augmenting Noam's answer:</p>

<p>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)$. </p>

<p>We therefore have a map:
$ T A \times T B \xrightarrow {dblstr} T(A\times B) \xrightarrow{uncurry(f)} TC $ </p>

<p>If we instantiate this to the continuation monad, we obtain your construction.</p>

<p>Generalizing to $n$-variables, the following should work (I didn't check all the details through). </p>

<p>Once we choose a permutation $\pi$ over $n$, we have a $\pi$-strength morphism $str_{\pi} : T A_1 \times \cdots \times T A_n \to T(A_1 \times \cdots \times A_n)$. (The monad laws should guarantee that it doesn't matter how we associate this permutation.) Therefore, for every $n$-ary morphism $f : A_1 \times \cdots \times A_n \to C$, we can construct:
$\gamma f : TA_1 \times \cdots \times TA_n \xrightarrow{str_{\pi}} T(A_1 \times \cdots \times A_n) \xrightarrow{Tf} TC$. </p>

<p>But I still don't think this really gives you the answer you're looking for...</p>

CC BY-SA 3.0
2014-09-18T14:59:35.910Z
2014-09-18T15:05:08.743Z
2014-09-18T15:05:08.743Z
Ohad Kammar
<p>Recall the continuation passing transform (CPS transform) which takes $A$ to $\beta A \mathrel{{:}{=}} R^{R^A}$ (where $R$ is fixed) and $f : A \to B$ to $\beta f : \beta A \to \beta B$ defined by
$$\beta \, f \, \kappa \, r \mathrel{{:}{=}} \kappa (r \circ f).$$
In fact we have the <em>continuation monad</em> with the unit $\eta_A : A \to \beta A$ defined by
$$\eta_A x \mathrel{{:}{=}} \lambda r . r \, x$$
and the multiplication $\mu_A : \beta (\beta A) \to \beta A$ defined by
$$\mu_A \, K \, r \mathrel{{:}{=}} K (\lambda f . f \, r).$$</p>

<p>Now let us think about how we can transform a <em>binary</em> map $f : A \to B \to C$, i.e, we want $\gamma f : \beta A \to \beta B \to \beta C$. One quickly comes up with
$$\gamma \, f \, \kappa \, \nu \, r \mathrel{{:}{=}}
   \kappa (\lambda x . \beta (f x) \nu r).$$
This makes sense from a programming point of view as well.</p>

<p>Here is my question: is there a deeper reason for $\gamma$, other than the fact that it looks right from a programming point of view? For instance, is there a category-theoretic or other "theoretical" reason for thinking that $\gamma$ makes sense? For instance, can we cook up $\gamma$ from the monad in a systematic way?</p>

<p>I am looking for an insight into CPS transforms of $n$-ary functions.</p>

CC BY-SA 3.0
2013-09-12T21:17:44.657Z
Are you looking for something beyond Haskell's `liftM2` or generalizations to `Applicative`? You can derive an n-ary version of what you describe (in a language that lets you talk about n-ary polymorphic functions) directly from the continuation applicative structure.
copumpkin
CC BY-SA 3.0
2013-09-12T22:01:05.537Z
I know how to write these generalizations, I want to know *why* they are like that. Category theorists will understand what I am asking.
Andrej Bauer
CC BY-SA 3.0
2013-09-12T22:01:57.150Z
Hmm, thanks for pointing out `Applicative`. It has `liftA2` which is my $\gamma$, see http://hackage.haskell.org/packages/archive/base/4.2.0.0/doc/html/Control-Applicative.html#v%3AliftA2
Andrej Bauer
CC BY-SA 3.0
2013-09-12T23:01:43.040Z
Yeah, `liftA2` was part of what I was suggesting. The "idiom bracket" notion (`(| f x y z ... |)` translates to `pure f <*> x <*> y <*> z <*> ...`) from `Applicative` seems like the systematic way to get the n-ary form of your question. I know the CT, but it seemed simplest to talk about it in standard programming terms. If you hadn't come across `Applicative` before, you might want to look at lax monoidal functors (although Haskell's statement of it with `<*>` involves exponentials as well). Anyway, I don't have an answer for you but was trying to better understand what you were getting at :)
copumpkin
CC BY-SA 3.0
2013-09-13T08:21:16.097Z
Hayo Thielecke's PhD thesis is on the categorical structure of CPS. Maybe the answer lies there or in his other publications. http://www.cs.bham.ac.uk/~hxt/research/hayo-thielecke-publications.shtml
Dave Clarke
CC BY-SA 3.0
2013-09-13T19:16:47.437Z
expanding on copumpkin's approach we can get n-ary lifting in general from any monoidal (and thus closed) functor between two closed monoidal categories.
sclv
CC BY-SA 3.0
2013-09-14T08:44:20.633Z
Does the lifting satisfy a universal property?
Andrej Bauer
<functional-programming><monad><continuations><cps-transforms>
Continuation passing transform of binary functions
Andrej Bauer
# Continuation passing transform of binary functions

(Asked by: username_0 on 2013-09-12)

Recall the continuation passing transform (CPS transform) which takes $A$ to $\beta A \mathrel{{:}{=}} R^{R^A}$ (where $R$ is fixed) and $f : A \to B$ to $\beta f : \beta A \to \beta B$ defined by
$$\beta \, f \, \kappa \, r \mathrel{{:}{=}} \kappa (r \circ f).$$
In fact we have the *continuation monad* with the unit $\eta\_A : A \to \beta A$ defined by
$$\eta\_A x \mathrel{{:}{=}} \lambda r . r \, x$$
and the multiplication $\mu\_A : \beta (\beta A) \to \beta A$ defined by
$$\mu\_A \, K \, r \mathrel{{:}{=}} K (\lambda f . f \, r).$$

Now let us think about how we can transform a *binary* map $f : A \to B \to C$, i.e, we want $\gamma f : \beta A \to \beta B \to \beta C$. One quickly comes up with
$$\gamma \, f \, \kappa \, \nu \, r \mathrel{{:}{=}}
\kappa (\lambda x . \beta (f x) \nu r).$$
This makes sense from a programming point of view as well.

Here is my question: is there a deeper reason for $\gamma$, other than the fact that it looks right from a programming point of view? For instance, is there a category-theoretic or other "theoretical" reason for thinking that $\gamma$ makes sense? For instance, can we cook up $\gamma$ from the monad in a systematic way?

I am looking for an insight into CPS transforms of $n$-ary functions.

**Tags:** functional-programming, monad, continuations, cps-transforms

> **Comments:**
> **username_1**: Are you looking for something beyond Haskell's `liftM2` or generalizations to `Applicative`? You can derive an n-ary version of what you describe (in a language that lets you talk about n-ary polymorphic functions) directly from the continuation applicative structure.  
> **username_0**: I know how to write these generalizations, I want to know *why* they are like that. Category theorists will understand what I am asking.  
> **username_0**: Hmm, thanks for pointing out `Applicative`. It has `liftA2` which is my $\gamma$, see http://hackage.haskell.org/packages/archive/base/4.2.0.0/doc/html/Control-Applicative.html#v%3AliftA2  
> **username_1**: Yeah, `liftA2` was part of what I was suggesting. The "idiom bracket" notion (`(| f x y z ... |)` translates to `pure f <*> x <*> y <*> z <*> ...`) from `Applicative` seems like the systematic way to get the n-ary form of your question. I know the CT, but it seemed simplest to talk about it in standard programming terms. If you hadn't come across `Applicative` before, you might want to look at lax monoidal functors (although Haskell's statement of it with `<*>` involves exponentials as well). Anyway, I don't have an answer for you but was trying to better understand what you were getting at :)  
> **username_2**: Hayo Thielecke's PhD thesis is on the categorical structure of CPS. Maybe the answer lies there or in his other publications. http://www.cs.bham.ac.uk/~hxt/research/hayo-thielecke-publications.shtml  
> **username_3**: expanding on username_1's approach we can get n-ary lifting in general from any monoidal (and thus closed) functor between two closed monoidal categories.  
> **username_0**: Does the lifting satisfy a universal property?  

---

## 2 answers

### Answer by username_4 on 2013-12-28. Score: 7

The closest I've seen to an answer to this question is the first picture in [the Gallery of Doctor Melliès](http://www.pps.univ-paris-diderot.fr/~mellies/gallery.html),
![~~A * ~~B |- ~~(A * B)](https://i.sstatic.net/lqhD9.jpg)
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 binary functions reduces to applying this map and then composing with the functorial action of the double-negation monad.

The illustration basically follows the standard conventions of [string diagrams](http://ncatlab.org/nlab/show/string+diagram) (modulo the polarizations of the wires, which are meant to indicate the flow of control). In particular, the map is constructed in three steps: twice applying the [strength](http://ncatlab.org/nlab/show/tensorial+strength) ($\kappa\wedge$) of the monad induced from the negation self-adjunction, and then applying the counit of the adjunction ($\epsilon$). At this level of abstraction, the derivation is generic for any adjunction giving rise to a strong monad, and you could then ask for a more abstract characterization of such adjunctions, which Melliès has also [written about](http://www.pps.univ-paris-diderot.fr/~mellies/tensorial-logic/8-parametric-monads-and-enriched-adjunctions.pdf).


---

### Answer by username_5 on 2014-09-18. Score: 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 to the continuation monad, we obtain your construction.

Generalizing to $n$-variables, the following should work (I didn't check all the details through).

Once we choose a permutation $\pi$ over $n$, we have a $\pi$-strength morphism $str\_{\pi} : T A\_1 \times \cdots \times T A\_n \to T(A\_1 \times \cdots \times A\_n)$. (The monad laws should guarantee that it doesn't matter how we associate this permutation.) Therefore, for every $n$-ary morphism $f : A\_1 \times \cdots \times A\_n \to C$, we can construct:
$\gamma f : TA\_1 \times \cdots \times TA\_n \xrightarrow{str\_{\pi}} T(A\_1 \times \cdots \times A\_n) \xrightarrow{Tf} TC$.

But I still don't think this really gives you the answer you're looking for...


---

