markdown 来自卑微起点的Yoneda直觉

Posted 2021-05-05

(previous [Yoneda blog](https://gist.github.com/Icelandjack/aecf49b75afcfcee9ead29d27cc234d5))
([reddit](https://www.reddit.com/r/haskell/comments/a0nyjj/yoneda_intuition_from_humble_beginnings/))
([twitter](https://twitter.com/Iceland_jack/status/1067173831708688384))

# 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`](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor.html#v:fmap) and [`id`](https://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Function.html#v: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."
> 
> [*What You Needa Know about Yoneda*](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/proyo.pdf)

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

## Yoneda; Term level

```haskell
[1..3]
```

Every list can be expressed as a (higher-order) function by viewing it through our Yoneda-tinted glasses :

```haskell
\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:

```haskell
  (\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:

```haskell
  \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

```haskell
\post -> Just (post True)
\_    -> Nothing
```

And the Yoneda form of [`Const "abc"`](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Const.html#t:Const) doesn't touch the string:

```haskell
\_ -> 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`:

```haskell
\post -> \bool -> post (not bool)
```

So we are really postcomposing `not` with our `post` function:

```haskell
\post -> post . not
\post -> fmap post not
```

or, doing case analysis on the Boolean, we are invoking `post` on the negated Boolean.

```haskell
\post -> \case    -- -XLambdaCase
  False -> post True
  True  -> post False
```

What happens when we pass in `id`? We get back `not`:

```haskell
\case
  False -> True
  True  -> False
```

## Yoneda; Type level

Our first example used `Functor []`

```haskell
list :: [Int]
list = [1..3]
```

So what is the type of the Yoneda form? (switching back from `post` to `f`)

```haskell
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](https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.html#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 (no I don't know archercy, so this will be a funky). I think of `Yoneda [] Int` (Yoneda form of `[Int]`) like a cocked crossbow: we have "pulled" the `Int` out of it we get a very tightly-strung `(Int -> x)`, leaving a list of holes `[x]`.

To fire we load it with a *1)* type `@Int` and *2)* function (arrow) `id :: Int -> Int`
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](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application)

    ```haskell
    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,

```haskell
just :: Maybe Bool
just = Just True
```
becomes
```haskell
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:
```haskell
yoNothing :: (a -> x) -> Maybe x
yoNothing _ = Nothing
```

Similarly `constAbc` contains no values of `a` 
```haskell
constAbc :: Const String a
constAbc = Const "abc"
```
so 
```haskell
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
```haskell
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;

```haskell
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

```haskell
show @Int :: (->) Int String
```

and `flip fmap show` (`(<$> show)`) pulls the `String` back

```haskell
(<$> show @Int) :: (String -> x) -> (Int -> x)
```

But the same doesn't work for `Int`, up until now we have worked on **co**variant arguments but `String` appears **contra**variantly. To understand the difference compare the type of `fmap` and [`contramap`](https://hackage.haskell.org/package/contravariant-1.5/docs/Data-Functor-Contravariant.html#v:contramap): the only difference is that the input arrow is flipped:

```haskell
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`](https://hackage.haskell.org/package/kan-extensions-5.2/docs/Data-Functor-Yoneda.html) 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):

```haskell
(a -> x) -> (F a -> F x)
```

What is the type of `flip (fmap @F)`?

```haskell
F a -> (a -> x) -> F x
```
or if you wish to be explicit
```haskell
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`

```haskell
                 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`

```haskell
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`](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-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`](https://hackage.haskell.org/package/kan-extensions-5.2/docs/Data-Functor-Yoneda.html#t: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 

```haskell
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
```