Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Last active April 8, 2024 11:08
Show Gist options
  • Save Icelandjack/02069708bc75f4284ac625cd0e2ec81f to your computer and use it in GitHub Desktop.
Save Icelandjack/02069708bc75f4284ac625cd0e2ec81f to your computer and use it in GitHub Desktop.
Yoneda Intuition from Humble Beginnings

(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.

  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 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
@freddie-freeloader
Copy link

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!

@Icelandjack
Copy link
Author

Oof glad you liked it!

@domenkozar
Copy link

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
Copy link

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
Copy link

qrilka commented Dec 4, 2018

Probably s/archercy/archery/?

@Icelandjack
Copy link
Author

Thanks, fixed those two issues

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment