13
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – copumpkin Sep 12 '13 at 21:17
  • 1
    $\begingroup$ I know how to write these generalizations, I want to know why they are like that. Category theorists will understand what I am asking. $\endgroup$ – Andrej Bauer Sep 12 '13 at 22:01
  • 1
    $\begingroup$ Hmm, thanks for pointing out Applicative. It has liftA2 which is my $\gamma$, see hackage.haskell.org/packages/archive/base/4.2.0.0/doc/html/… $\endgroup$ – Andrej Bauer Sep 12 '13 at 22:01
  • 3
    $\begingroup$ 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 :) $\endgroup$ – copumpkin Sep 12 '13 at 23:01
  • 2
    $\begingroup$ Hayo Thielecke's PhD thesis is on the categorical structure of CPS. Maybe the answer lies there or in his other publications. cs.bham.ac.uk/~hxt/research/hayo-thielecke-publications.shtml $\endgroup$ – Dave Clarke Sep 13 '13 at 8:21
7
$\begingroup$

The closest I've seen to an answer to this question is the first picture in the Gallery of Doctor Melliès, ~~A * ~~B |- ~~(A * B) 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 (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 ($\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.

$\endgroup$
4
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.