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:
- What exactly is the difference between the two?
- Is there something I can do with one that can't be done with the other?
- Why is the universal quantification needed at all for
backward
?
In Haskell we write lambdas for the values we pass:
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
which means: the caller should choose and pass a type
@a
, then a value of that typex :: @a
and finally receive that value backx
.Now, your issue arises from the two (isomorphic) types
Here,
T
does not depend ona
. 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: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.
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:On top, GHC can re-generalize the type, hence we obtain
Not really.
Usually, when defining an isomorphism between
A
andB
we wantIf either type has a forall (say,
A = forall r . V r
) then we get a forall in that position. Note that the type forback
in this case is also isormoprhic towhich 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.)