map f . map g = map (f.g)

map_f_map_g_equals_map_f_g.hs

-- ============================================================ --
--
--                map f . map g = map (f.g)
--
-- ============================================================ --

-- ============================================================ --
--
-- CATEGORICAL PROGRAMMING WITH INDUCTIVE AND COINDUCTIVE TYPES
-- 
-- Calculating with folds
--
-- ============================================================ --
--
-- definition of foldr 
--
foldr :: (a -> b -> b) -> b -> [a] -> b 
foldr f b []     = b 
foldr f b (x:xs) = f x (foldr f b xs)

-- identity law 
-- foldr (:) [] = id

-- fusion law
-- h (f a b) = g a (h b) => h . foldr f b = foldr g (h b)

--
-- an application for map
--

--
-- identity law  : map id = id
--
map id
=  by def of map
foldr (\x xs -> id x : xs) []
=  by id x = x
foldr (\x xs -> x : xs) []
=  by def of (:)
foldr (:) []
=  by identity law
= id

--
-- fusion law  : map p . map q = map (p . q)
--
map p . map q
=                                     by using def of map q
map p . foldr (\x xs -> q x : xs) []
|       |     |                   |   h = map p, f = (\x xs -> q x : xs), b = []; (*1)
h     . foldr f                   b
=                                     by using  h . foldr f b = foldr g (h b) 
foldr g (h     b )
|     |  |     |                      by (*1)
foldr g (map p [])
=                                     by map p [] = []
foldr g []
=
foldr g                       []
=     |                               by g = \x xs -> p (q x) xs; see below
foldr (\x xs -> p (q x) : xs) []
=                                     by def of (.)
foldr (\x xs -> (p.q) x : xs) []
=                                     by def of map
map (p . q)

--
-- find g by using h (f a b) = g a (h b)
--
h     (f                  a b )
|      |                  | |         by (*1)
map p ((\x xs -> q x :xs) a [])
=
map p (q a : [])
=
foldr (\x xs -> p x : xs) [] (q a : [])
=
(\x xs -> p x : xs) (q a) (foldr (\x xs -> p x : xs) [] [])
=
(\x xs -> p x : xs) (q a) (map p [])
=
p (q a) : map p []
=                                     by def of (:) 
(\x xs -> p (q x) : xs) a (map p [])
|                       |  |     |    by (*1)
g                       a (h     b )

g = \x xs -> p (q x) : xs


-- ============================================================ --
--
-- A tutorial on the universality and expressiveness of fold
--
-- 3.2 The fusion property of fold
--
-- ============================================================ --

(1) h w = v 
(2) h (g x y) = f x (h y)
 =>
    h fold g w = fold f v

(1)
map f []      = []
|     |         |
h     w       = v

(2)
map f (g x:y)                        = (f . g) x : map f y
map f (\x xs ->   x : xs) (g x) y    = (\x xs -> x         : xs) (f . g x) (map f y)
map f (\x xs -> g x : xs) x     y    = (\x xs -> (f . g) x : xs) x         (map f y)
|     |                   |     |      |                         |          |     |
h     g                   x     y    = f                         x          h     y

=>
map f . map g
=
map f . fold (\x xs -> g x : xs) []
|       |    |                   |
h       fold g                   w 
=
fold f                         v
|    |                         |
fold (\x xs -> (f . g) x : xs) []
=
map (f . g)