haskellcategory-theoryforall

How to understand the universal quantification in Yoneda's natural isomorphism?

While learning about the Yoneda lemma, I came across the following encoding of the underlying natural isomorphism in Haskell:

forward  :: Functor f => (forall r . (a -> r) -> f r) -> f a
forward  f = f id

backward  :: Functor f => f a -> (forall r. (a -> r) -> f r)
backward  x f = fmap f x

I tried to simplify the implementation of backward to flip fmap but failed as the latter has type f a -> (a -> r) -> f r.

From here on I'm stuck in pinpointing what precisely are the differences between the two implementations. More so as applying either function to a concrete functor yields the same result type:

ghci> :t bw (Just "") 
bw (Just "") :: (String -> r) -> Maybe r

ghci> :t (flip fmap)  (Just "") 
(flip fmap)  (Just "") :: (String -> r) -> Maybe r

Questions:

Solution

  • In Haskell we write lambdas for the values we pass:

    id :: forall a . a->a
id = \x -> x

    but when we compile to the lower-level Core language, which is closed to System F, we also see type lambdas. The code becomes more like

    id = \ @a (x :: @a) -> x

    which means: the caller should choose and pass a type @a, then a value of that type x :: @a and finally receive that value back x.

    Now, your issue arises from the two (isomorphic) types

    forall a . T -> U a
--  vs
T -> forall a . U a

    Here, T does not depend on a. The two types are indeed isomorphic, and at the lower level it's just a matter of "flipping" the term-lambda with the type-lambda:

    \ @a (x :: T) -> ...  -- has the former type
-- vs
\ (x :: T) @a -> ...  -- has the latter

    Since in Haskell we do not usually write or see the type-lambdas, it is hard to distinguish between these. Further, when the compiler performs type inference it will (as far as I can understand) infer the first one, where the type-lambdas are all at the beginning.

    What exactly is the difference between the two?

    Not much. They have isomorphic types, after all. One has the forall a at the topmost level, while the other has it in another position.

    Once you apply then to arguments as you did, GHC will automatically choose the right place to add the inferred @a argument, so you won't easily notice the difference. The two calls are of these forms:

    f @r x
-- vs
f x @r

    On top, GHC can re-generalize the type, hence we obtain

    (\@r -> f @r x) :: forall r . ....
(\@r -> f x @r) :: forall r . ....

    Is there something I can do with one that can't be done with the other?

    Not really.

    Why is the universal quantification needed at all for backward?

    Usually, when defining an isomorphism between A and B we want

    forw :: A -> B
back :: B -> A

    If either type has a forall (say, A = forall r . V r) then we get a forall in that position. Note that the type for back in this case is also isormoprhic to

    forall r . B -> V r

    which is what we would get if we omitted the quantifier (and let Haskell re-add it implicitly at the top-level).

    (By contrast, the quantifier in the type of forw :: (forall r . V r) -> B can not be moved to the top level.)