law of composition.hs

-- We want to prove this:
fmap (compose g f)  ==  compose (fmap g) (fmap f)

-- Fact:
fmap :: (b -> c) -> (a -> b) -> (a -> c)
compose :: (b -> c) -> (a -> b) -> (a -> c)

-- Prove
fmap id f
(\ h g x -> h (g x)) id f
(\ g x -> id (g x)) f
(\ x -> id (f x))
(\ x -> f x)
-- using eta-conversion we got that (\x -> f x) is the same as f
f

-- let see how can we beta reduce this
fmap (compose g f) a
-- that equivalent by saying
compose (compose g f) a
-- compose is (\ g f a -> g (f a)) or usin alpha conversion
-- we can say taht (\g f a -> g (f a)) is the same with (\i h b -> i (h b))
-- or change the symbol as long as the pattern still the same

-- so
(\g f a -> g (f a)) ((\g f a -> g (f a)) g f) a
-- is the same as
(\i h b -> i (h b)) ((\k j c -> k (j c)) g f) a
-- and let beta reduce this!
(\i h b -> i (h b)) ((\j c -> g (j c)) f) a
-- we can still reduce it 
(\i h b -> i (h b)) (\c -> g (f c)) a
-- and again
(\h b -> (\c -> g (f c)) (h b)) a
-- and again yeay
\b -> (\c -> g (f c)) (a b)
-- one more time
\b -> g (f (a b))
-- YEAAYYY
fmap (compose g f) a == \b -> g (f (a b))


-- let's do it on the second equation
compose (fmap g) (fmap f) a
-- in lambda we can do this
(\i h b -> i (h b)) ((\k j c -> k (j c)) g)
                    ((\m l d -> m (l d)) f)
                    a
                    
-- and reduce it
(\i h b -> i (h b)) (\j c -> g (j c))
                    ((\m l d -> m (l d)) f)
                    a

-- and this
(\i h b -> i (h b)) (\j c -> g (j c))
                    (\l d -> f (l d))
                    a

-- one more
(\h b -> (\j c -> g (j c)) (h b)) (\l d -> f (l d)) a

-- again
(\b -> (\j c -> g (j c)) ((\l d -> f (l d)) b)) a

-- one more
(\j c -> g (j c)) ((\l d -> f (l d)) a)

-- another more
(\j c -> g (j c)) (\d -> f (a d))

-- yes we can still reduce it
\c -> g ((\d -> f (a d)) c)
-- we can change the lambda function inside d still it is c
\c -> g (f (a c))
-- and done!
-- so
compose (fmap g) (fmap f) a == \c -> g (f (a c))

-- TIME TO CHECK!
fmap (compose g f)  ==  compose (fmap g) (fmap f)

\b -> g (f (a b)) == \c -> g (f (a c))

-- using alpha conversion, we can see those are the same!