{{ message }}

Instantly share code, notes, and snippets.

# Icelandjack/Yoneda_II.markdown

Last active Aug 21, 2021
Yoneda Intuition from Humble Beginnings

# 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 `Int`s. 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.

1. 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]`
2. 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 `fmap`s 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```

### Icelandjack commented Nov 26, 2018

Consider donating despite the lazy structure https://www.patreon.com/Iceland_jack

### freddie-freeloader commented Nov 28, 2018

This is starting to feel ranty, I will discuss how to actually use Yoneda later

Well that's quite a cliffhanger. 😄

A great read so far though!

### domenkozar commented Nov 28, 2018

Great stuff! Could I recommend http://nbviewer.jupyter.org/github/gibiansky/IHaskell/blob/master/notebooks/IHaskell.ipynb to make it more interactive in next post? :)

### jegi commented Nov 29, 2018

Thanks for the link! But the quotation that the Yoneda Lemma is "arguably the most important result in category theory" is due to Emily Riehl, not to us.

### qrilka commented Dec 4, 2018

Probably `s/archercy/archery/`?

### Icelandjack commented May 12, 2020

Thanks, fixed those two issues