Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
map f . map g = map (f.g)
-- ============================================================ --
--
-- 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)
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.