Yoneda lemma for fmap fusion

gistfile1.hs

--------------------------------------------------
-- Yoneda lemma

newtype Yoneda f a =
    Yoneda (forall b. (a -> b) -> f b)
    -- Nat (Hom(a, -), F) ~~ F a
    
-- this is `liftYoneda`
yoneda :: (Functor f) => f a -> Yoneda f a
yoneda x = Yoneda $ \f -> fmap f x

-- this is `lowerYoneda`
unYoneda :: (Functor f) => Yoneda f a -> f a
unYoneda (Yoneda y) = y id

instance Functor (Yoneda f) where
    -- Yoneda f a = forall r. (a -> r) -> f r
    -- f :: a -> b
    -- y :: forall r. (a -> r) -> f r
    -- g :: (b -> r)
    -- g . f :: a -> r
    -- y (g . f) :: f r
    fmap f (Yoneda y) = Yoneda $ \g -> y (g . f)

-- fmap fusion for free with Yoneda!
-- Let us have the following variables
lst :: [a], g :: a -> b, f :: b -> c
-- Without Yoneda:
map f . map g $ lst
-- With Yoneda:
unYoneda . fmap f . fmap g. yoneda $ lst
-- From this, using equational reasoning, we can get:
unYoneda . fmap f $ fmap g (yoneda lst)
-- definition of `yoneda`
unYoneda . fmap f $ fmap g (Yoneda $ \k -> fmap k lst)
-- `Functor` instance for `Yoneda`
unYoneda . fmap f $ (Yoneda $ \h -> (\k -> fmap k lst) (h . g))
-- Beta-reduction
unYoneda . fmap f $ (Yoneda $ \h -> fmap (h . g) lst)
-- `Functor` instance for `Yoneda`
unYoneda $ (Yoneda $ \k -> (\h -> fmap (h . g) lst) (k . f))
-- Beta-reduction
unYoneda $ (Yoneda $ \k -> fmap (k . f . g) lst)
-- `unYoneda` definition
(\k -> fmap (k . f . g) lst) id
-- Beta-reduction
fmap (id . f . g) lst
-- `Functor` instance for lists + id law
map (f . g) lst

Thanks a lot for this!

I assume those beta-reduction steps are done by the compiler?

Edwin Jose Palathinkal

@edwinhere, I am actually not so sure. I guess GHC can optimize some beta-redexes away. Even if it doesn't, the real optimization here is that the Yoneda version does not traverse the structure several times