luqui’s answer is excellent but I’m going to offer another explanation of forall b. (a -> b) -> b === a for a couple reasons: First, because I think the generalization to Codensity is a bit overenthusiastic. And second, because it’s an opportunity to tie a bunch of interesting things together. Onwards!
z5h’s Magic Box
Imagine that someone flipped a coin and then put it in a magic box. You can’t see inside the box but if you choose a type b and pass the box a function with the type Bool -> b, the box will spit out a b. What can we learn about this box without looking inside it? Can we learn what the state of the coin is? Can we learn what mechanism the box uses to produce the b? As it turns out, we can do both.
We can define the box as a rank 2 function of type Box Bool where
type Box a = forall b. (a -> b) -> b
(Here, the rank 2 type means that the box maker chooses a and the box user chooses b.)
We put the a in the box and then we close the box, creating… a closure.
-- Put the a in the box.
box :: a -> Box a
box a f = f a
For example, box True. Partial application is just a clever way to create closures!
Now, is the coin heads or tails? Since I, the box user, am allowed to choose b, I can choose Bool and pass in a function Bool -> Bool. If I choose id :: Bool -> Bool then the question is: will the box spit out the value it contains? The answer is that the box will either spit out the value it contains or it will spit out nonsense (a bottom value like undefined). In other words, if you get an answer then that answer must be correct.
-- Get the a out of the box.
unbox :: Box a -> a
unbox f = f id
Because we can’t generate arbitrary values in Haskell, the only sensical thing the box can do is apply the given function to the value it is hiding. This is a consequence of parametric polymorphism, also known as parametricity.
Now, to show that Box a is isomorphic to a, we need to prove two things about boxing and unboxing. We need to prove that you get out what you put in and that you can put in what you get out.
unbox . box = id
box . unbox = id
I’ll do the first one and leave the second as an exercise for the reader.
unbox . box
= {- definition of (.) -}
\b -> unbox (box b)
= {- definition of unbox and (f a) b = f a b -}
\b -> box b id
= {- definition of box -}
\b -> id b
= {- definition of id -}
\b -> b
= {- definition of id, backwards -}
id
(If these proofs seem rather trivial, that’s because all (total) polymorphic functions in Haskell are natural transformations and what we’re proving here is naturality. Parametricity once again provides us with theorems for low, low prices!)
As an aside and another exercise for the reader, why can’t I actually define rebox with (.)?
rebox = box . unbox
Why do I have to inline the definition of (.) myself like some sort of cave person?
rebox :: Box a -> Box a
rebox f = box (unbox f)
(Hint: what are the types of box, unbox, and (.)?)
Identity and Codensity and Yoneda, Oh My!
Now, how can we generalize Box? luqui uses Codensity: both bs are generalized by an arbitrary type constructor which we will call f. This is the Codensity transform of f a.
type CodenseBox f a = forall b. (a -> f b) -> f b
If we fix f ~ Identity then we get back Box. However, there’s another option: we can hit only the return type with f:
type YonedaBox f a = forall b. (a -> b) -> f b
(I’ve sort of given away the game here with this name but we’ll come back to that.) We can also fix f ~ Identity here to recover Box, but we let the box user pass in a normal function rather than a Kleisli arrow. To understand what we’re generalizing, let’s look again at the definition of box:
box a f = f a
Well, this is just flip ($), isn’t it? And it turns out that our other two boxes are built by generalizing ($): CodenseBox is a partially applied, flipped monadic bind and YonedaBox is a partially applied flip fmap. (This also explains why Codensity f is a Monad and Yoneda f is a Functor for any choice of f: The only way to create one is by closing over a bind or fmap, respectively.) Furthermore, both of these esoteric category theory concepts are really generalizations of a concept that is familiar to many working programmers: the CPS transform!
In other words, YonedaBox is the Yoneda Embedding and the properly abstracted box/unbox laws for YonedaBox are the proof of the Yoneda Lemma!
TL;DR:
forall b. (a -> b) -> b === a is an instance of the Yoneda Lemma.