Categories for Programmers: The Yoneda Lemma

http://bartoszmilewski.com/2015/09/01/the-yoneda-lemma/

by hectorxp • 11 years ago

109 29 11 years ago

andrzejsz2• 11 years ago

Quicker than me congrats :)

kazinator4• 11 years ago

Can someone kindly explain this in terms of word-sized chunks of data made of bits, grinding through a Von Neumann machine, perhaps illustrated using C code snippets?

kbenson2• 11 years ago

I really wish we had a better statically typed language that a large percentage of programmers knew (or knew enough of) that we could use instead as a sort of pseudo-code.

I find C's quirk's end up taking all my attention when trying to grok something interesting expressed in C.

sink• 11 years ago

you mean like Haskell?

danidiaz• 11 years ago

Not that I fully understand it, but this post https://golem.ph.utexas.edu/category/2008/01/the_continuatio... establishes a connection between the Yoneda lemma and continuation-passing style, with C (well, C++) code.

kmicklas• 11 years ago

This isn't about "word-sized chunks of data made of bits, grinding through a Von Neumann machine". It's about math and software engineering.

If this article is hard to understand, that's probably because it's part 14 of a series. Read the first 13 parts; Bartosz's writing is very clear when you have the proper context.

kazinator4• 11 years ago

It's about math and software engineering.

Good idea; can you explain it in terms of software engineering? What software engineering problem is it solved by this lemma?

E.g. Starting with this set of requirements, we are transported to a solution thusly: ...

wz10002• 11 years ago

If you do the same for the Mediator pattern.

tel5• 11 years ago

Mediator just about creating a stable API. The various mediated objects offer functionality, the mediator makes a common (and stable) interface against that functionality. Consumers only see the mediator and this leaves you free to change the mediated objects out if needed.

So it's the same thing as always: make a stable API and code against it.

tel5• 11 years ago

Ever used CPS style? Instead of producing values and passing them back to callers you provide continuations to functions and then they never return, merely calling the continuation instead. It turns out that this can save a lot of stack space and it also turns out that you can convert any program into this style should you choose.

It might not be exactly clear why CPS is equivalent to "direct" style. The answer is the Yoneda Lemma.

Yoneda goes further. Normally you could maybe notate a CPS style function as follows

    (a -> *) -> *

where `a` is the type of the value the computation will pass to the continuation function (the first argument here) and * is a special type indicating "will never return". We can generalize this slightly as

    forall x . (a -> x) -> x

which enables us to talk about CPS'd code in a slightly more general way by not stating exactly what the continuation does—it produces some kind of value, which might be the "will never return" value, and the CPS'd function just needs to evaluate it because the forall is positioned such that it can't know what `x` is. This gives more power to the user of CPS'd functions.

We can generalize it again by writing

    forall x . (a -> x) -> F x

which gives more power to the implementer of the CPS'd function by letting them return some kind of "effect structure" along with calling the handler. The effect structure is fixed ahead of time but lets us talk about

    * calling the continuation multiple times
    * returning failure via exceptions
    * producing side effects
    * producing default values when no `a` ever existed
    * etc.

And in this most general setting Yoneda still comforts us that this is just equivalent to the "direct" form

F a

kazinator4• 11 years ago

I think it's clearer if you don't bring in the lemma. Calling the continuation is the same as returning a value: both are just a jump that restores the stack pointer and communicates a value. (The continuation just keeps the stack below the stack pointer instead of discarding it.) (Could it be that it's because continuations have certain properties that they fall under the lemma?)

The commutative diagrams, rather, remind me of diagrams that I remember from chemistry. We can go from this molecule to that one via this path or that one, and the energy deltas are the same.

Speaking of continuations, I'm currently looking at porting the trick used by some OCaml people of doing delimited continuations on the C stack, into my own language. It's pretty neat: just copy the C stack into a closure-like object, and then when you need to invoke the continuation, swap that segment back onto the regular linear stack (into a stable space prepared using alloca). Rebuild some exception handling chains through this new pieces of stack, and then invoke the thing using an exception (ultimately a longjmp). When it is done running, you can blow it away. All permanent effects are in external environments that are on the heap. The next time you call into it, you just copy it in the same way.

I'm unclear on how you can do a longjmp to something that has been copied elsewhere on the stack relative to its original location. I mean, the jmp_buf probably has an absolute stack pointer in it which it restores. I have to look at their code again; the obvious hack is to scan the jmp_buf for values that look like pointers into the stack area and adjust those values.

I implemented a stack copying hack once to get a 64 bit Linux kernel on MIPS to call into 32 bit firmware, passing ordinary local variables (whose addresses are 64 bit values on a 64 bit stack) to the firmware functions. I copied the kernel thread's stack into a buffer 32 bit addressable space. Then I adjusted all internal pointers within that stack to point to the correct places in the new location. The threads's pointer was then thunked into that space around the call to the firmware. The firmware API wrapper was then seeing data addresses whose lowest 32 bits could be passed down to the firmware routines via 32 bit registers and still point to the correct data. Of course, a reverse copy from the faked stack was then done to retrieve any results which the firmware routine wrote into local buffers. This worked well enough that I was able to expose boot firmware environment variables through a /proc interface (even making it writable!) Based on such past experience, I'm confident I can do this delimited continuation hack.

dkarapetyan• 11 years ago

Nope, can't be done. You'd basically need to build up an entirely different language for manipulating symbols to even make any sense of it. That new language would look very much like ML, Coq, Agda, Haskell, etc.

I think people forget that it's ok to not know any of this stuff. You can spend an entire lifetime writing nothing but Java and you won't miss out on anything.

There is no reason to understand this beyond the technical challenge of understanding it. It will never be useful in any actual day-to-day software engineering endeavor because whatever you can do with the Yoneda lemma you can do without it and the Yoneda lemma does not make the solution any better, it does not make reasoning about large scale dynamic systems any easier, and it will not make your software less prone to bugs.

kazinator4• 11 years ago

You'd basically need to build up an entirely different language for manipulating symbols to even make any sense of it.

No problem:

  struct symbol {
    obj_base_fields; // macro
    obj name_string;
    obj package;
    // ...
  };

  struct cons {
    obj_base_fields; // macro
    obj car, cdr;
  };

AnimalMuppet• 11 years ago

Well... it might help, sometimes.

I think about something like Stokes' theorem: The integral of a function over the boundary of a manifold is equal to the integral of the derivative of the function over the interior of the manifold. But in practice, one integral or the other is often easier to do; that means that the theorem has the practical effect of letting you transform some hard problems into equivalent but easier problems.

But note well that I said "some problems". There are many problems that this won't help with. There are others where the problem you're trying to solve is the easier one, and applying the theorem turns it into a harder problem.

I suspect (but do not know) that the Yoneda Lemma is similar. It can sometimes give you a simpler way of looking at a problem. But just sometimes. Sometimes the Haskell/ML view is the easiest way to solve the problem you have. And sometimes it's not.

whateveracct• 11 years ago

If you think that's what 'for programmers' means, then lol

mordocai2• 11 years ago

Started reading this, was confused, thought "WTH this is for programmers(not computer scientists)?". Then realized it is part 14. Oh well, guess I need to start at part 1...

andrzejsz2• 11 years ago

Yes but it is fairly approachable and indeed it was written in progeammers in mind

mordocai2• 11 years ago

Oh yeah, I wasn't meaning to complain really. It just made no sense to me because I hadn't already read part 1 - 13 I'm sure.

asdftemp• 11 years ago

a simpler introduction http://blog.sigfpe.com/2006/11/yoneda-lemma.html

backlava• 11 years ago

Programmers, yo don't neda lemma.

jonnybgood• 11 years ago

This reminded of an OCamlers critique of Haskell [1], which I think raises a very good point:

Yoneda-crazy: I know Haskell, I know some category theory, but I am highly sceptical that teaching the Yoneda Lemma to C++ programmers is actually useful in any way. I am the first to applaud the idea of scientific curiosity, of learning fun stuff of unclear usefulness just for the fun of it, but I think that a few excellent writers and tinkerers have given the Haskell community as a whole (and the foreigners that receive some of its TV shows by satellite) the wrong impression that the theoretical underpinning of typed functional programming is category theory. I would say that (1) it's a gross over-simplification of what the theory of typed functional programming is about, emphasizing a small part of it that has enabled some people to do very interesting things and (2) it is highly likely to be absolutely useless to an overwhelming large majority of the readers of such popularization material. Category Theory is fashionable these days, and I find the fashion aspect irritating -- it may be that I'm just bitter? I'm worried that we may have a backslash at some point when, you know, people realize that unless your initials are E.K. you are wasting your time thinking about the co-density transformation. On the other hand, this category circus has been going on for years, and I believe nobody has been hurt so far, so maybe it's just fine.

[1] https://www.reddit.com/r/ocaml/comments/3ifwe9/what_are_ocam...

tel5• 11 years ago

He was pretty directly referencing Dr. Milewski, I'm sure. He's a relatively famous C++ guy from my understanding who of late has been doing this whole category theory for programmers series.

Which is a shame because the whole series is gold.

Categories for Programmers: The Yoneda Lemma

Related Stories