Icelandjack/Yoneda_II.markdown

## Yoneda_II.markdown

      
    Raw
  

              Yoneda_II.markdown
            
          
    (previous Yoneda blog)
(reddit)
(twitter)
Yoneda Intuition from Humble Beginnings

Let's explore the Yoneda lemma. You don't need to be an advanced Haskeller to understand this. In fact I claim you will understand the first section fine if you're comfortable with map/fmap and id.
I am not out to motivate it, but we will explore Yoneda at the level of terms and at the level of types.

"[Yoneda lemma], arguably the most important result in category theory."
Emily Riehl

(congratulations on not running away after "Yoneda lemma" or "category theory", what are you on)
Yoneda; Term level

[1..3]
Every list can be expressed as a (higher-order) function by viewing it through our Yoneda-tinted glasses 🕶:
\f -> [f 1, f 2, f 3]
It's like the function f grabs a hold of each element. I'll call it post because it does "postprocessing".
The Yoneda lemma states that [1..3] and \f -> [f 1, f 2, f 3] are equivalent! (naturally isomorphic)
How do we go back? We pass it the identity function:
  (\post -> [post 1, post 2, post 3]) id
= [id 1, id 2, id 3]
= [1..3]
The Yoneda form of [1..3] can be understood without (f)map but it is really map partially applied to its second argument:
  \post -> [post 1, post 2, post 3]
= \post -> map post [1..3]
= flip map [1..3]
= (<$> [1..3])
This works for any Functor, the Yoneda forms of Just True and Nothing are
\post -> Just (post True)
\_    -> Nothing
And the Yoneda form of Const "abc" doesn't touch the string:
\_ -> Const "abc"
Recall that functions are Functors too (instance Functor ((->) a) where fmap = (.)), which is where our head starts to hurt: The Yoneda form now transforms a function to a higher-order function, how does that work?
Let's take the function not as an example, we pass the result of not bool to post:
\post -> \bool -> post (not bool)
So we are really postcomposing not with our post function:
\post -> post . not
\post -> fmap post not
or, doing case analysis on the Boolean, we are invoking post on the negated Boolean.
\post -> \case    -- -XLambdaCase
  False -> post True
  True  -> post False
What happens when we pass in id? We get back not:
\case
  False -> True
  True  -> False
Yoneda; Type level

Our first example used Functor []
list :: [Int]
list = [1..3]
So what is the type of the Yoneda form? (switching back from post to f)
yoList :: (Int -> x) -> [x]
yoList f = [f 1, f 2, f 3]
Interesting. Is this what you expected?
Before we had a list of Ints. Now we have a polymorphic higher-order function. The polymorphism is crucial for this to work, (warning: vague) think of it as grabbing every Int inside of [Int] and ripping them out, leaving a hole x behind (not to be confused with typed holes, this is a conceptual hole) (bonus points if you physically act this out every time you use Yoneda).
Imagine we have a magical Yoneda crossbow (I don't know archery). I think of Yoneda [] Int (Yoneda form of [Int]) like a cocked crossbow: we have "pulled" the Int out of it, it's now a tightly-strung arrow Int -> x waiting to fire the values into [x].
In effect, beause of the polymorphism, there are two arguments. The type x (invisible) and the arrow Int -> x (visible).
The choice of arrow is important but the type is no less important, instanting the type to @String firing the arrow show :: Int -> String gives a list of strings:
  yoList @String show :: [String]
= ["1", "2", "3"]
Choosing @Int as the type and \a -> 2 * a * a as the arrow yields yet another expression
  yoList @Int \a -> 2 * a * a :: [Int]
= [2, 8, 18]
But something special happens when we fire at @Int with the arrow id :: Int -> Int. We get back the original list.


Remember that yoList :: forall x. (Int -> x) -> [x] actually takes x as an invisible argument. GHC usually solves it with unifiation but our first step is to instantiate x with a type: with crucial use of the yoList polymorphism we pick Int using visible type applications
yoList @Int :: (Int -> Int) -> [Int]


The second step is passing id :: Int -> Int (..the arrow?) as an argument, and we get yoList @Int id :: [Int] back.


Let's look at the other cases,
just :: Maybe Bool
just = Just True
becomes
yoJust :: (Bool -> x) -> Maybe x
yoJust f = Just (f True)
Nothing :: Maybe a contains no values of type a but, but we can still follow the pattern:
yoNothing :: (a -> x) -> Maybe x
yoNothing _ = Nothing
Similarly constAbc contains no values of a
constAbc :: Const String a
constAbc = Const "abc"
so
yoConstAbc :: (a -> x) -> Const String x
yoConstAbc _ = Const "abc"
You might ask, "what happens if we do want to change the String?". So far I have restricted myself to Functor which is very limiting. See if you can make sense of the type of \f -> Const (f "abc") or even
yoPair :: (Int -> x) -> (x, x)
yoPair f = (f 1, f 2)
which is not a Haskell Functor. We can in fact play this game with arbitrary type parameters;
pair :: (Int, Bool, Char)
pair = (10, False, 'X')

yoPair1 :: (Int -> x) -> (x, Bool, Char)
yoPair1 f = (f 10, False, 'X')

yoPair2 :: (Bool -> y) -> (Int, y, Char)
yoPair2 f = (10, f False, 'X')

yoPair123 :: (Int -> x) -> (Bool -> y) -> (Char -> z) -> (x, y, z)
yoPair123 f g h = (f 10, g False, h 'X')
etc. are you getting a feel for it yet? To go back, we pass id.
Functions get weird though, when we have a function show @Int the type is
show @Int :: (->) Int String
and flip fmap show ((<$> show)) pulls the String back
(<$> show @Int) :: (String -> x) -> (Int -> x)
But the same doesn't work for Int, up until now we have worked on covariant arguments but String appears contravariantly. To understand the difference compare the type of fmap and contramap: the only difference is that the input arrow is flipped:
fmap      :: Functor       f => (a -> a') -> (f a -> f a')
contramap :: Contravariant f => (a <- a') -> (f a -> f a')
Yoneda; Type level again

This is starting to feel ranty, I will discuss how to actually use Yoneda later (for example to fuse fmaps or to derive right Kan extensions), but for now I leave you with the type of fmap @F (I'm jumping around with variable names):
(a -> x) -> (F a -> F x)
What is the type of flip (fmap @F)?
F a -> (a -> x) -> F x
or if you wish to be explicit
forall a x. F a -> (a -> x) -> F x
It kind of looks like F a and F x are having a tug-o-war using (a -> x). Of course that's not what is happening at all, perish the thought. But if we float the forall x past F a
                 vvvvvvvvvvvvvvvvvvvvvvvvv
forall a. F a -> forall x. (a -> x) -> F x
                 ^^^^^^^^^^^^^^^^^^^^^^^^^
we got ourselves the type of our Yoneda forms. Because our yo* examples had to be polymorphic in the x
yoList          :: forall   x. (Int    -> x) -> [x]
yoJust          :: forall   x. (Bool   -> x) -> Maybe x
yoNothing       :: forall a x. (a      -> x) -> Maybe x
yoConstAbc      :: forall a x. (a      -> x) -> Const String x
(<$> show @Int) :: forall   x. (String -> x) -> (Int -> x)
so with RankNTypes we can give Yoneda a name (I use a type synonym for simplicity, you will want to use a newtype like Data.Functor.Yoneda)
>> :set -XRankNTypes
>> type Yoneda f a = (forall xx. (a -> xx) -> f xx)
>>
>> :t (\f -> [f 1, f 2, f 3]) :: Yoneda [] Int
.. :: (Int -> xx) -> [xx]
>> :t (<$> [1..3]) :: Yoneda [] Int
.. :: (Int -> xx) -> [xx]

and now we
yoList          ::           Yoneda []             Int
yoJust          ::           Yoneda Maybe          Bool
yoNothing       :: forall a. Yoneda Maybe          a
yoConstAbc      :: forall a. Yoneda (Const String) a
(<$> show @Int) ::           Yoneda ((->) Int)     String