Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Yoneda lemma for fmap fusion
--------------------------------------------------
-- 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
@ghost

This comment has been minimized.

Copy link

@ghost ghost commented Jun 17, 2014

Thanks a lot for this!

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

Edwin Jose Palathinkal

@co-dan

This comment has been minimized.

Copy link
Owner Author

@co-dan co-dan commented Jun 17, 2014

@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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.