The continuation passing transform and the Yoneda embedding

Posted in Category theory, Math, Programming by Mike Stay on 2007 December 19

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

 CPT_f( (*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 C^{\rm op} and produces a category \mbox{HOM}(C, \mbox{Set}):

\begin{array}{ccccccc}\mbox{CPT}: & C^{\rm op} & \to & \mbox{HOM}(C, \mbox{Set}) \\ & A & \mapsto & \mbox{hom}(A, -) \\ & f:B\leftarrow A & \mapsto & \mbox{CPT}(f): & \mbox{hom}(B, -) & \to & \mbox{hom}(A, -) \\ & & & & k & \mapsto & k \circ f \end{array}

We get the transformation above by uncurrying to get \mbox{CPT}(f):\mbox{hom}(B, -) \times A \to -.

In Java, a (cartesian closed) category C is an interface C with a bunch of internal interfaces and methods mapping between them. A functor F:C \to {\rm Set} 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 {\rm CPT\langle X\rangle}:C \to {\rm Set}. We’d write

class CPT<X> implements C.

Then each internal interface C.A gets instantiated as a set CPT.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.f described above.

Then the Yoneda lemma says that for every model of C—that is, for every class F implementing the interface C—there’s a natural isomorphism between the set F(A) and the set of natural transformations {\rm hom}({\rm hom}(A, -), F).

A natural transformation \alpha between F:C \to {\rm Set} and {\rm CPT\langle X \rangle}:C \to {\rm Set} 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.

9 Responses

Subscribe to comments with RSS.

  1. summerstay said, on 2007 December 23 at 6:47 am

    Continuation passing: transform and roll out!

  2. ccshan said, on 2007 December 25 at 7:56 am

    The closest explanation of the Yoneda lemma to what you wrote that I’ve seen is sigfpe’s ( but it still doesn’t use the word “continuation”.

  3. reperiendi said, on 2007 December 25 at 1:25 pm

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

  4. bosullvn said, on 2008 January 11 at 10:11 pm

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

  5. sigfpe said, on 2008 January 22 at 4:49 pm

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

  6. reperiendi said, on 2008 January 22 at 5:34 pm

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

  7. […] This embedding is better known among computer scientists as the continuation passing style transformation. […]

  8. nextdress said, on 2019 January 9 at 6:18 am

    Hi! The link to Chris Barker’s work (“Continuations in Natural Language”) seems dead, and I’m having trouble getting the PDF from Would you happen to know where I could get it?

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: