The Continuation Passing Transform and the Yoneda Embedding

January 10, 2008

The Continuation Passing Transform and the Yoneda Embedding

Posted by John Baez

$MathML-enabled post (click for more details).$

Guest post by Mike Stay

The Yoneda embedding is familiar in category theory. The continuation passing transform is familiar in computer programming.

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

$MathML-enabled post (click for more details).$

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 $C^{op}$ and produces a category $HOM(C, Set):$

$\array{CPT: & C^{op} & \to & HOM(C, Set) \\ & A & \mapsto & hom(A, -) \\ & f:B\leftarrow A & \mapsto & CPT(f): & hom(B, -) & \to & hom(A, -) \\ & & & & k & \mapsto & k \, \mathrm{o} \, f}$

We get the transformation above by uncurrying to get $CPT(f):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 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 parametrized functor $CPT\langle X\rangle:C \to Set$ . 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 $C$ —that is, for every class F implementing the interface C—there’s a natural isomorphism between the set $F(A)$ andthe set of natural transformations $hom(hom(A, -), F).$

A natural transformation $\alpha$ between $F:C \to Set$ and $CPT:C \to 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.

Posted at January 10, 2008 8:01 AM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1568

27 Comments & 1 Trackback

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

a (cartesian closed) category $C$ is an interface $C$ with a bunch of internal interfaces and methods mapping between them

It seems to me that, by itself, the interface is more like a graph, and implementing the interface establishes a graph morphisms from that graph to the graph underlying the category of sets.

The reason is that the interface makes no specification about the result of composing any of the methods it declares.

Just recently I saw on some blog, but I forget where (yours maybe??), a discussion of how categories appear in Java and/or C++.

There I saw this point addressed: the author identified the composition operation in the category with a kind of consistency checking that some programming languages apparently have. I forget the programming language termininology. Something like “tests” or the like. You need to help me here.

The point being that, if you define an interface which specified one data type A and three methods $f,g,h : A \to A$ which each read in an $A$ and spit out an $A$ , you want to be able to say things like $g \circ f = h \,.$

The interface alone does not do that.

And in fact that seems to be pretty hard to implement in a programming language. It should even be impossible, right? The compiler would have to check, whenever you instantiate an interface, if the methods in the class implementing the interface satisfy this composition property. But each method is a program in its own right. So checking this amounts to checking correctness of programs, right? Which is in general impossible, right?

(Stop me if I am spouting nonsense, I am not a computer science expert.)

Posted by: Urs Schreiber on January 10, 2008 2:55 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

It seems to me that, by itself, the interface is more like a graph, and implementing the interface establishes a graph morphisms from that graph to the graph underlying the category of sets.

The reason is that the interface makes no specification about the result of composing any of the methods it declares.

Just recently I saw on some blog, but I forget where (yours maybe??), a discussion of how categories appear in Java and/or C++.

Yes, you can find my article here. I was trying to avoid the details of that in this post, so I just stated the conclusion.

You’re absolutely right: a Java interface can’t specify relations between morphisms. I fell back on a notion of “tests” to try to make up for it.

And in fact that seems to be pretty hard to implement in a programming language. It should even be impossible, right? The compiler would have to check, whenever you instantiate an interface, if the methods in the class implementing the interface satisfy this composition property. But each method is a program in its own right. So checking this amounts to checking correctness of programs, right? Which is in general impossible, right?

Yep. And even if you’re just dealing with circuits, which have a fixed running time, you’re dealing with a co-NP problem (show that this circuit always outputs false).

In my article, I said the functions had to pass the tests on all inputs, but as you note, there are no universal quantifiers. So what typically happens is people write small functions and test those on a few inputs, then hope that their small function isn’t complicated enough to mess up in places they haven’t tested.

Many programmers advocate writing tests first: what is it, exactly, that you expect of this program? Then when all the tests pass, you quit writing code—most programmers have a tendency to write code they think they’ll use, but never do, and this style avoids wasting time.

Another technique supposes that you’re willing to deal with errors up front, but want some assurance of future behavior. For instance, suppose you have a data compressor (like gzip). Gzip is a complicated beast of a program with no thought given to proving correctness. It would be a real challenge to prove anything about the code. However, say you would like to be certain that data, once compressed, will always decompress correctly, but you’re willing to deal with errors at compression time.

The compressor may depend on data that is not in the file to be compressed; perhaps it uses the time of day to seed a random number generator for a genetic algorithm or some such. If the decompressor can be shown to depend only on the data in the file to decompress, then you can compress the data, decompress it, and give an error message if they’re different. Assuming you got no error at that point, then the compressed file must always decompress correctly.

So while you can’t actually impose relations on morphisms, you can come close a lot of the time.

Posted by: Mike Stay on January 10, 2008 5:29 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

$g \circ f$

It seems that \circ is used far more on this blog to denote composition than to denote degrees. The appropriate symbol is [◦], but even if I try to use it directly, it gets converted wrong in a latex environment [ $◦$ ].

Posted by: Mike Stay on January 10, 2008 5:49 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

> the author identified the composition operation in the category with a kind of consistency checking that some programming languages apparently have.

Loosely speaking, In the category of types and (computer) functions, composition is what you expect it to be, composition of functions. But in order to compose arrows the source of one must match the target of the other. Ensuring that this holds at all points in a program is known as type-checking, and all statically-typed programming languages (Java, Haskell, C++) have some sort of type checking. But I don’t know if this was the category being referred to.

Anyway, that aside, there isn’t really a “the CPS transform” but there are many of them. The Curry-Howard isomorphism sets up a correspondence between (pure) functional programming languages and intuitionistic logic. On this isomorphism you can think of a program written in a language with continuations as corresponding to classical logic. The Godel-Gentzen translation (among others) embeds classical logic in intuitionistic logic. Isomorphically, the Godel-Gentzen CPS transform embeds programming with continuations into pure functional programming. (You get one CPS transform for each embedding of classical logic into intuitionistic logic.)

This correspondence between logic and programming is one of the most amazing things to come out of computer science. One time I took a textbook on (classical) logic and by applying the Curry-Howard isomorphism to it it turned into a book on writing compilers. I’m not exaggerating, I documented every step of the way here. But you need to know Haskell to make sense of that.

But I hadn’t realised there was a Yoneda lemma connection. I need to think about that.

Incidentally, I wrote a short explanation of some connections between the Yoneda lemma and (Haskell) programming here and here.

Posted by: Dan Piponi on January 11, 2008 10:08 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Loosely speaking, In the category of types and (computer) functions, composition is what you expect it to be, composition of functions.

Yes, but that’s different from the identfication of C++/Java interfaces with categories that Mike Stay is talking about in the above entry.

Posted by: Urs Schreiber on January 12, 2008 12:18 AM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

> Yes, but that’s different from the identfication of C++/Java interfaces with categories that Mike Stay is talking about in the above entry.

Not really. In fact, I think Mike’s saying the same thing as me here except that I don’t call functions of type (a->b)->b continuations, even though that’s the standard way to represent them in Haskell. In fact, Mike’s just plugged a little hole in my understanding of continuations which I think is really cool.

Posted by: Dan Piponi on January 22, 2008 11:54 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Loosely speaking, In the category of types and (computer) functions, composition is what you expect it to be, composition of functions.

Yes, but that’s different from the identfication of C++/Java interfaces with categories that Mike Stay is talking about in the above entry.

Not really.

But there is no notion of composition of methods in a Java interface.

Mike suggested above

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

with each method being a morphism.

But that’s not quite right. The interface (as opposed to its implementation!) makes no statements whatsoever about the result of composing any two methods it defines.

So when the interface defines a method

$B f(A a);$

it says that there is an edge from type $A$ to type $B$ called $f$

$A \stackrel{f}{\to} B$

but if you have, say, two other such edges $C g(B b);$

and

$C h(A a);$

there is no way to even ask the question whether or not the composite of $f$ with $g$ might equal $h$ , let alone answer it.

In fact, the interface does not even demand that when

$A \stackrel{f}{\to} B$ and $B \stackrel{g}{\to} C$ are methods it defines, that it must also define any method from $A$ to $C$ .

But without all that, the arrows $f,g,h$ are not morphisms in a category. They are edges in a graph, though.

$category - composition = graph \,.$

Mike Stay did agree with that, by the way. As we discussed above, following his suggestion, one can save the intended identification of Java interfaces with categories to some extent by invoking “tests”.

Posted by: Urs Schreiber on January 23, 2008 8:44 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

The strange thing is that on my misreading of Mike, the Yoneda lemma does apply and it gives an isomorphism between the types a and forall b.((a->b)->b). And that does say something interesting about continuations.

Posted by: Dan Piponi on January 24, 2008 11:01 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

I don’t think you’re misreading me; I think perhaps you and Urs are misreading each other and you’re both in vociferous agreement.

The “continuation passing transform” I refer to is the one described, for instance, in the wikipedia article on continuation passing (in first paragraph past the example code). It’s the same as the embedding of call-by-value into call-by-name described here at the bottom of page 1.

I need to read your paper more carefully to understand it, as I haven’t learned Haskell yet. It sounds like someone is being sloppy in what they call a CPS transform.

Following some links around, I see that Wadler has a paper on how the (a?) CPS transform is a Galois connection (which sounds interesting: I have no idea what that is) and something about a dual logic (does that have anything to do with the reflection I talked about on my blog?)

I’ll get this all sorted out in my head someday…

Posted by: Mike Stay on January 25, 2008 1:32 AM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Ding! The light goes on!

Call-with-current-continuation is double negation. Many programming languages don’t have it, but you can always convert to continuation passing style and simulate it. This is an embedding of classical logic into intuitionistic logic.

Consider how to represent “NOT P” as a proposition if all we’ve got is implication and FALSE:

(1)

P \to FALSE.

The contrapositive of $P \to Q$ is

(2)

(Q \to FALSE) \to (P \to FALSE).

But what if we don’t even have FALSE? Let $X$ be some type. Then we can define

(3)

P \to X

for any $X$ , and the contrapositive of $P\to Q$ is

(4)

(Q \to X) \to (P \to X),

which is the Yoneda embedding.

I’m still not exactly sure how to get from double negation to call-cc, but it’s getting a lot clearer.

Posted by: Mike Stay on January 26, 2008 3:01 AM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

A morphism $f:X \to Y$ in a cartesian closed category is (according to Lambek) a pair $(x:X, \phi(x):Y),$ where $x$ is free in $\phi:X \to Y.$ Since $\cdot:I$ is free in all terms, a constant term $x:X$ is a pair $(\cdot:I, x:X).$

Given a constant term $a:A$ , i.e. a morphism $a:I\to A$ , the Yoneda embedding gives

(1)

CPT(a)_X:hom(A,X) \to hom(I,X).

Uncurry, braid, and recurry to get

(2)

CPT(a)_X:I \to hom(hom(A,X),X),

i.e. a term of type

(3)

(A\to X)\to X

that’s naturally isomorphic. This is the double negation!

Languages with call-cc automatically apply the Yoneda embedding functor and then make available the magical “holodeck” term call-cc that allows you to jump back in time (“backtracking”).

It’s magical in exactly the same way as a function with “side-effects”–given a functor that adjoins an environment:

(4)

TA = A \times E

you have more functions $A\times E \to B\times E$ than $A \to B$ (assuming $E$ has more than one element). From the point of view of a function that has been “lifted” into the larger realm with the functor $T,$ these others appear “magical” because they don’t depend exclusively on $A.$

Posted by: Mike Stay on January 26, 2008 4:43 AM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Call-cc comes from the identity function:

(1)

1:hom(A,X)\to hom(A,X)

Uncurry, braid, recurry to get

(2)

call-cc:A \to hom(hom(A,X),X).

Posted by: Mike Stay on January 26, 2008 5:02 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Sorry, that’s wrong: at least in Scheme, call-cc expects something of type ((A->X)->X) and passes in the current continuation as the first parameter. So call-cc isn’t the magical term, it’s the continuation that’s passed in by call-cc that appears magical.

Posted by: Mike Stay on January 26, 2008 9:58 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

call/cc’s type is Peirce’s law: $((A \to \bot) \to A) \to A$ . Together with ex falso you can obtain from this the rule of double-negation elimination. Personally I think that Peirce’s law is one of the weirdest clasical tautologies I’ve ever seen. But you can actually derive it from the intuitional semantics of call/cc — your current continuation (c.c.) expects a value of type, say, $A$ , so the continuation’s type is $A \to \bot$ . call/cc’s argument is a function that takes the c.c. — $(A\to\bot)\to B$ . What is $B$ ? Well, call/cc actualy returns, and it must return $A$ , but where can it possibly get $A$ ? Only from applying its argument to the c.c.! And that implies $B$ and $A$ are the same thing, and call/cc type is $((A \to \bot) \to A) \to A$ , q.e.d.

But I still like the DNE-rule better, because it’s just a slightly modified ex falso. Indeed, ex falso rule is $\frac{\Gamma \vdash \bot}{\Gamma\vdash \phi},$ and DNE is $\frac{\Gamma, \phi\to\bot \vdash \bot}{\Gamma\vdash \phi}.$ So from the computational point of view, it’s just an “abort”/”throw” operator which also receives the c.c. when invoked and returns the value of the type which the c.c. expected.

Posted by: Joker_vD on August 19, 2013 2:37 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Mike wrote:

… a Galois connection (which sounds interesting: I have no idea what that is)

Yes you do — you just don’t know it! A ‘Galois connection’ is just a scary name for a pair of adjoint functors. People mainly use this term for adjoint functors between categories that are mere posets.

The classic example goes back to — surprise! — Galois. Here’s how it goes:

Given any field $K$ , any subfield $k \subseteq K$ determines a group called $Gal(K | k)$ , which is just the subgroup of symmetries of $K$ that fix every element of $k$ .

The bigger $k$ is, the smaller this group is.

Conversely, given any subgroup of the symmetries of $K$ , we get a subfield $k$ : just take all the elements fixed by that subgroup.

The bigger this subgroup is, the smaller the subfield is.

So, we get (upside-down) maps going back and forth between:

the poset of subgroups of the symmetry group of $K$

and:

the poset of subfields of the field $K$

and these are, in fact, adjoint functors!

The great thing is that none of this has anything to do with ‘fields’. If you got scared when I said ‘fields’, just replace the word ‘field’ above with the name of pretty much whatever mathematical gadget you want, and it still works! It’s a super-general, super-beautiful idea.

Posted by: John Baez on January 25, 2008 7:55 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Is it possible for a functor to be its own adjoint? (I’m thinking of the CPS transform as a reflection…)

Posted by: Mike Stay on January 25, 2008 9:43 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Mike wrote:

Is it possible for a functor to be its own adjoint?

Sure! Any equivalence $F: C \to C$ can be made into its own left and right adjoint. That’s because any equivalence can be promoted to an ‘adjoint equivalence’. But, there are also more spicy examples.

I’m too busy writing our paper (ahem) to pay much attention to what you’re doing here, but you mentioned ‘double negation’, and that reminds me of the contravariant functor you get in any compact symmetric monoidal category $C$ namely the functor sending any object $X\in C$ to its dual $X^*$ . This gives an equivalence $* : C \stackrel{\sim}{\to} C^{op}$ which can be promoted to an adjoint equivalence. And taking the dual twice is naturally isomorphic to the identity functor! So, there’s a strong relation between this sort of dualization and ‘negation’… and geometrically speaking, ‘reflection’.

Posted by: John Baez on January 26, 2008 3:33 AM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

Posted by: Dan Piponi on January 24, 2008 11:01 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

In fact, the interface does not even demand that when

(1)

A\stackrel{f}{\to} B

and

(2)

B\stackrel{g}{\to} C

are methods it defines, that it must also define any method from A to C.

Well, you can talk about the composition of methods in any class that implements the interface, without mentioning a specific implementation, so the interface kind of implicitly has a notion of a path in a graph. So interfaces give you the free category on a graph and tests (sort of) give you relations.

Posted by: Mike Stay on January 25, 2008 1:12 AM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

By the way, my impression is that mathematicians are usually not aware that Yoneda is a computer scientist. He was a teacher of my friend Makoto Matsumoto, who himself spends part of this time on computer science, another part on rice farming, and the rest on arithmetic fundamental groups.

Posted by: Minhyong Kim on January 11, 2008 9:21 AM | Permalink | Reply to this

What about delimited continuations?

Raw continuations are a little too wild in practice. Linear continuations are fine (ie continuations that can only be used once; apply Curry-Howard to linear logic and then use double-linear-negation to get continuations) though. But even that’s a bit too much.

On the other hand, delimited continuations (read Oleg’s many writings on this topic) are closer to what is actually done in practice. Certainly, the kind of continuations that one encounters routinely in operating systems, co-routines, etc [see Oleg’s work for the details] are all delimited. So, in a categorical setting what does that correspond to?

Posted by: Jacques Carette on January 29, 2008 2:01 AM | Permalink | Reply to this

Re: What about delimited continuations?

$MathML-enabled post (click for more details).$

According to the intro paragraph in “Delimited continuations in operating systems,” a delimited continuation is just one that receives an input, processes it a little, and passes the result to another continuation.

In the statement

(1)

print(1 + 2 \times 3),

the “1+” part receives the result of $2\times 3,$ increments it, and passes the result to print().

So it’s just the Yoneda embedding of a single morphism as part of a composite morphism. (Since the Yoneda embedding is a functor, it preserves composition.)

Posted by: Mike Stay on January 29, 2008 5:30 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

There’s an interesting way to do continuations that doesn’t reflect the structure; rather, it flattens the structure but puts in markers to know how to rebuild it.

In this style,

(1)

(f\,((g\,x)\,y)) \rightarrow c \mapsto (((((((c T)\,\overline{f})\,T)\,T)\,\overline{g})\,\overline{x})\,\overline{y})

Since the structure is flat, we can drop the parens to get

(2)

T\,\overline{f}\,T\,T\,\overline{g}\,\overline{x}\,\overline{y}

which is the same as dropping the right parens from the original expression. Since all the applications are binary, we didn’t need them in the first place.

The term $T$ is rather complicated:

(3)

T = c,L \mapsto (L\,(l,R \mapsto (R\,(r \mapsto (c\,(l\,r)))))

The type of $T$ is also rather convoluted:

(4)

T:(B \to C) \to (((A \to B) \to ((A \to C)\to D)\to D)\to E) \to E

Does anyone recognize this?

Posted by: Mike Stay on March 8, 2008 12:58 AM | Permalink | Reply to this

Read the post The Pi Calculus II
Weblog: The n-Category Café
Excerpt: Mike Stay begins to explain the pi calculus.
Tracked: September 8, 2009 4:53 PM

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

This thread was misleading for me for quite a while, but I finally received some clarification on two key points:

The category theoretic corollary of delimited continuations is not the Yoneda embedding, but another right Kan extension: codensity. In other words, as opposed to undelimited continuations they universally quantify B in (A -> B) -> B.
Neither of these are equivalent to double negation or Peirce’s law as Curry Howard proves an equivalence with intuitionistic logic where the theorem of double negation isn’t true unless both A and B in (NOT A -> NOT B) -> NOT B are universally quantified.

Hope this helps.

Posted by: Sophia Gold on May 21, 2017 6:01 AM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

The two links named “even show up” and “in English” in the main post appear to be broken. May someone perhaps care to repair them?

Posted by: Peter Heinig on June 3, 2017 9:51 AM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Well, I don’t know if Barker himself has moved, but the NYU URLspace must certainly have changed sometime in the last nine years.

A gander at The Wikipedia brings up one or two of (some) Barker’s papers, for example PDF:Continuations and the nature of quantification and PDF:Continuations in Natural Language [extended abstract].

In the first paper, I think “NP” is short for “noun phrase”, so he isn’t claiming any insight on complexity theory… and that’s about as far as I’ve looked into that one. I can’t make much of the Extended Abstract, but the preamble of Section 3 flags itself as important:

The main problem of interest is what I call ‘scope displacement’: even when a quantificational expression such as everyone occurs in a deeply embedded position, the quantifier it contributes can take semantic scope over the entire sentence.

(4) a. John (saw everyone).
b. ∀ x: saw x j

Here, even though everyone is buried within the verb phrase saw everyone, in the paraphrase in (4b), the logical quantifier ∀ takes scope over the entire meaning. Continuations, of course, are superb at allowing a deeply embedded operator to take control over a larger expression in which it is embedded, and the analysis described here is based on that ability.

Posted by: Jesse C. McKeown on June 3, 2017 5:08 PM | Permalink | Reply to this

Re: The Continuation Passing Transform and the Yoneda Embedding

$MathML-enabled post (click for more details).$

Thanks for the explanations.

Posted by: Peter Heinig on June 11, 2017 2:13 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

January 10, 2008