## The continuation passing transform and the Yoneda embedding

They’re the same thing! Why doesn’t anyone ever say so?

Assume `A`

and `B`

are types; the continuation passing transform takes a function (here I’m using C++ notation)

B f(A a);

and produces a function

<X> CPT_f(<X> (*k)(B), A a) { return k(f(a)); }

where `X`

is any type. In `CPT_f`

, instead of returning the value `f(a)`

directly, it reads in a continuation function `k`

and “passes” the result to it. Many compilers use this transform to optimize the memory usage of recursive functions; continuations are also used for exception handling, backtracking, coroutines, and even show up in English.

The Yoneda embedding takes a category and produces a category :

We get the transformation above by uncurrying to get

In Java, a (cartesian closed) category is an interface `C`

with a bunch of internal interfaces and methods mapping between them. A functor is written

`class F implements C`

.

Then each internal interface `C.A`

gets instantiated as a set `F.A`

of values and each method `C.f()`

becomes instantiated as a function `F.f()`

between the sets.

The continuation passing transform can be seen as a parameterized functor . We’d write

`class CPT<X> implements C`

.

Then each internal interface `C.A`

gets instantiated as a set `CPT`

`<X>`

`.A`

of methods mapping from `C.A`

to `X`

—i.e. continuations that accept an input of type `C.A`

—and each method `C.f`

maps to the continuized function `CPT<X>.f`

described above.

`Then the Yoneda lemma says that for every model of —that is, for every `

`class F`

implementing the `interface C`

—there’s a natural isomorphism between the set and the set of natural transformations

A natural transformation between and is a way to cast the class `F`

to the class `CPT<X>`

such that for any method of `C`

, you can either

- invoke its implementation directly (as a method of
`F`

) and then continuize the result (using the type cast), or - continuize first (using the type cast) and then invoke the continuized function (as a method of
`CPT<X>`

) on the result

and you’ll get the same answer. Because it’s a natural *isomorphism*, the cast has an inverse.

The power of the Yoneda lemma is taking a continuized form (which apparently turns up in lots of places) and replacing it with the direct form. The trick to using it is recognizing a continuation when you see one.

summerstaysaid, on 2007 December 23 at 6:47 amContinuation passing: transform and roll out!

ccshansaid, on 2007 December 25 at 7:56 amThe closest explanation of the Yoneda lemma to what you wrote that I’ve seen is sigfpe’s (http://sigfpe.blogspot.com/2006/11/yoneda-lemma.html) but it still doesn’t use the word “continuation”.

reperiendisaid, on 2007 December 25 at 1:25 pmccshan: Yes, I saw that page. sigfpe has a lot of good stuff on his site. It surprises me that he wouldn’t mention continuation passing! Leinster’s paper on the Yoneda lemma is very nice if you already understand some category theory; it helped me understand how category theorists actually use the lemma, as I said in the last paragraph of the post.

Unfortunately, I’ve never had the opportunity to learn Haskell; I think if I were going to learn a language based on category-theoretic ideas, I’d go with O’Caml, because it runs at speeds comparable to C.

bosullvnsaid, on 2008 January 11 at 10:11 pmNice article, thank you. Regarding your last comment, Haskell runs at speeds comparable to both OCaml and C, so don’t dismiss it on the basis of performance. Of course it famously applies some category theoretic ideas to regular programming tasks, so you might find it a fruitful playground.

sigfpesaid, on 2008 January 22 at 4:49 pmI think you’re saying the same thing as me here except that I don’t mention that the type (a->b)->b corresponds to continuations because at that time I wasn’t yet thinking about continuations.

In fact, you’ve given me some deeper insight into continuations. The idea is this. In the context of continuations, the function ‘return’ maps from the type type a to the type (a->b)->b which can also be written Cont b a in Haskell. This (kind of) embeds a in Cont b a. That makes sense, Cont b a is like the value a but computed with a different style of programming, continuation passing style. But it always bothered me that it wasn’t an isomorphism because, as I say, it should just be the same thing coded up in a different way. But the missing piece is this: it *is* an isomorphism when you consider ‘return’ not as a function a -> ((a->b)->b) for some fixed b, but as a function polymorphic in b. In Haskell that’s written a -> (forall b . (a -> b) -> b) and that’s an isomorphism.

So thanks for helping me make the link between two different aspects of Haskell programming that I hadn’t connected together myself.

reperiendisaid, on 2008 January 22 at 5:34 pmYou’re welcome! This is one reason I really like category theory: it lets one make precise analogies between different areas of math, or look at the same structure from many points of view.

Yoneda embedding as contrapositive and call-cc as double negation « reperiendisaid, on 2008 January 26 at 2:46 pm[…] This embedding is better known among computer scientists as the continuation passing style transformation. […]