functorlaws

Proof of the functor laws for the Maybe functor 

fmap :: (a -> b) -> Maybe a -> Maybe b
fmap f (Just x) = Just (f x)
fmap f Nothing  = Nothing

Prove:
fmap id = id

Case 1: Just x

fmap id (Just x)
= Just (id x)    -- defn of fmap
= Just x         -- defn of id

Case 2: Nothing

fmap id Nothing
= Nothing        -- defn of fmap


Prove:
fmap (g . f) = fmap g . fmap f

Case 1: Just a
fmap (g . f) (Just a) 
= Just (g . f $ a)          -- defn of fmap
= Just (g(f a))             -- defn of .


(fmap g . fmap f) (Just a)
= fmap g (fmap f (Just a)) -- defn of .
= fmap g (Just (f a))      -- defn of fmap
= Just (g(f a))            -- defn of fmap


Case 2: Nothing
(fmap g . fmap f) Nothing 
= fmap g (fmap f Nothing) -- defn of .
= fmap g Nothing          -- defn of fmap
= Nothing                 -- defn of fmap

fmap (g . f) Nothing
= Nothing                 -- defn of fmap