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
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 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
.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 —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.
Continuation passing: transform and roll out!
The 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”.
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.
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.
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.
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.
[…] This embedding is better known among computer scientists as the continuation passing style transformation. […]
Hi! The link to Chris Barker’s work (“Continuations in Natural Language”) seems dead, and I’m having trouble getting the PDF from archive.org. Would you happen to know where I could get it?
His new homepage is here: https://www.nyu.edu/projects/barker/ The paper’s on his site and there’s a link to Amazon to purchase his book. I’ll update my links. Thanks!