posted by Darryl on 11 Feb 2015
Much has been written about the awesomeness that is the Yoneda Lemma. For instance, Edward Kmett said "When you need something to go faster, hit it with the Yoneda lemma. Still isn't fast enough? Use it again."
But what exactly is the Yoneda Lemma? What does it mean, and why does it mean that? That's what I'm going to address in this blog post, at least for the Haskell version of the lemma. If you're not familiar with Haskell, tho.. sorry.
Before we talk Yoneda, let's talk continuations. If I give you a value, let's say the integer
0, we can "lift" it by turning it into the function
\f -> f 0. This lifted form of
0 is just as good as
0 itself, because we can always apply this to
id and get
0 back out:
(\f -> f 0) id == id 0 == 0. So we can go back and forth between
0 and its lifted version all day — they're equivalent in an important sense.
Let's make this slightly more general, then:
lift :: forall a. a -> (forall b. (a -> b) -> b) lift x g = g x drop :: forall a. (forall b. (a -> b) -> b) -> a drop h = h id
The crucial bit here is that
forall b part: lifted values can continue towards anything. By "continue" I just mean the following sort of correspondence: given any program that contains
0, let's say the program
0 + 1, we can look at the program around
_ + 1) as a way to continue building a program starting with
0, and this naturally corresponds to pulling out a function as in
(\x -> x + 1) 0. This function tells us how to continue computing with a value, in this case,
0, and in this setting is called a "continuation".
A lifted value is just a value that has been lifted to take a continuation as input.
lift 0 $ \x -> x + 1
This code can be understood sort of by reading it as "start with 0, and continue by adding one to it". We can chain these things together in a nice way:
lift 0 $ \x -> lift (x + 1) $ \y -> lift (y * 2) $ \z -> ...
Or in English, start with 0, add it to 1, now multiply that by 2, then ...
drop function just says that if we have such a lifted value, there's always a trivial continuation for it: the one that does nothing at all and gives the number back:
lift 0 $ \x -> x == 0.
These two functions together therefore form an isomorphism: for every value of type
a there exists a function of type
forall b. (a -> b) -> b provided by
lift, and conversely, for every function of type
forall b. (a -> b) -> b there exists an
a provided by
drop, and moreover, this is a one-to-one correspondence.
To make it concrete: if I give you a function
h :: forall b. (Int -> b) -> b, then you know that this function must secretly be hiding an
Int inside somehow, because how else could it get out a
b, given just the
Int -> b input? If I specified
b = Void, which we're allowed to do because of the quantifier, the function can't just make an element of type
Void and return it, because there are no such elements. So how can I get a
Void out? The only way it could is to use its input and a hidden
So what does this have to do with the Yoneda Lemma? Well, simply, the Yoneda Lemma is a generalization of this ismorphism to functor-y types:
liftYo :: forall a f. Functor f => f a -> (forall b. (a -> b) -> f b) liftYo x g = fmap g x dropYo :: forall a f. Functor f => (forall b. (a -> b) -> f b) -> f a dropYo h = h id
The concrete version of this is more or less the same as for continuations. Supposing I again fix
a = Int, and also
f = , and I give you a function
h :: forall b. (Int -> b) -> [b], how can this possible give me a list of
bs just using a function of type
Int -> b? Obviously only if it has a list of
Ints tucked away somewhere that it can map over! And it doesn't matter what
f are, provided that there's some map-like functionality, hence the
Functor f constraint.
If you have comments or questions, get it touch. I'm @psygnisfive on Twitter, augur on freenode (in #languagengine and #haskell).