Proofs of functor laws in Haskell
Haskell defines a typeclass Functor containing a function fmap which allows developers to apply a function over the contents of an instance without changing the actual structure of the data (note that this is roughly equivalent to the formal definition of a functor). To achieve this guarantee, instances of Functor must obey the following two laws where fmap :: (a -> b) -> f a -> f b, id :: a -> a, f :: b -> c, and g :: a -> b:
fmap id == idfmap (f . g) == (fmap f . fmap g)
Proving these laws on different instances is a useful exercise, especially when you come up with your own instance for an arbitrary data structure and you need to verify that it is correct, so let’s prove them on two instances of Functor: Maybe a and [a]. For all the non-Haskellers out there, the former is a data structure that implements nullable values of a, and the latter is a list of a’s.
Nullable values: The Maybe a functor
A value of Maybe a is either Just a or Nothing; the instance should allow us to apply a function on either a in Just a or fail silently on Nothing without changing anything else. Therefore, fmap is defined as the following.
instance Functor Maybe where
fmap _ Nothing = Nothing (1)
fmap f (Just a) = Just (f a) (2)These proofs are fairly straightforward and follow the common theme of considering either case of Maybe a.
Proof of the first law
Claim: On m of Maybe a, fmap id m == id m.
Proof. On cases of m.
Case 1: m == Nothing.
fmap id m == fmap id Nothing {- by expansion of m -}
== Nothing {- by fmap (1) -}
== id m {- by definition of id, m -}Case 2: m == Just a.
fmap id m == fmap id (Just a) {- by expansion of m -}
== Just (id a) {- by fmap (2) -}
== Just a {- by expansion of id -}
== m {- by definition of m -}
== id m {- by definition of id -} ∎Proof of the second law
Claim: On m of Maybe a, fmap (f . g) m == (fmap f . fmap g) m.
Proof. On cases of m.
Case 1: m == Nothing.
fmap (f . g) m == fmap (f . g) Nothing
{- by expansion of m -}
== Nothing
{- by fmap (1) -}(fmap f . fmap g) m == fmap f (fmap g Nothing)
{- by expansion of (.) and m -}
== fmap f Nothing
{- by fmap (1) -}
== Nothing
{- by fmap (1) -}Case 2: m == Just a.
fmap (f . g) m == fmap (f . g) (Just a)
{- by expansion of m -}
== Just ((f . g) a)
{- by fmap (2) -}(fmap f . fmap g) m == fmap f (fmap g (Just a))
{- by expansion of (.), m -}
== fmap f (Just (g a))
{- by fmap (2) -}
== Just (f (g a))
{- by fmap (2) -}
== Just ((f . g) a)
{- by definition of (.) -}Therefore, fmap (f . g) m == (fmap f . fmap g) m in all cases. ∎
Lists: The [a] functor
The [a] functor should allow us to apply a function to every element of a list without changing anything else. Thus, fmap = map, which is defined as the following.
map :: (a -> b) -> [a] -> [b]
map _ [] = [] (1)
map f (x:xs) = f x : map f xs (2)The proofs here are a bit harder since lists have infinitely many cases to consider, so we must turn to induction.
Proof of the first law
Claim: On a list l, fmap id l == id l.
Proof. By induction on the length of l.
Base case: On a list where length l == 0, i.e. l = [].
fmap id l == map id [] {- by expansion of fmap, l -}
== [] {- by map (1) -}
== id [] {- by definition of id -}Inductive hypothesis: Assume that fmap id l’ == id l’ where length l’ < length l. Since l = x:xs where x and xs are the head and tail of l, respectively, fmap id xs == id xs as length xs < length l.
Inductive step:
fmap id l == map id (x:xs) {- by expansion of fmap, l -}
== id x : fmap id xs {- by map (2), defn. of fmap -}
== id x : id xs {- by inductive hypothesis -}
== x:xs {- by expansion of id -}
== id l {- by definition of id, l -} ∎Proof of the second law
Claim: On a list l, fmap (f . g) l == (fmap f . fmap g) l.
Proof. By induction on the length of l.
Base case: On a list where length l == 0 i.e. l = [].
fmap (f . g) l == map (f . g) []
{- by expansion of fmap, l -}
== []
{- by map (1) -}(fmap f . fmap g) l == map f (map g [])
{- by expansion of (.), fmap, l -}
== map f []
{- by map (1) -}
== []
{- by map (1) -}Inductive hypothesis: Assume that fmap (f . g) l’ == (fmap f . fmap g) l’ where length l’ < length l. Since l = x:xs where x and xs are the head and tail of l, respectively, fmap (f . g) xs == (fmap f . fmap g) xs as length xs < length l.
Inductive step:
fmap (f . g) l == map (f . g) (x:xs)
{- by expansion of fmap, l -}
== (f . g) x : fmap (f . g) xs
{- by map (2), definition of fmap -}(fmap f . fmap g) l == map f (map g (x:xs))
{- by expansion of (.), fmap, l -}
== map f (g x : map g xs)
{- by map (2) -}
== f (g x) : map f (map g xs)
{- by map (2) -}
== (f . g) x : fmap f (fmap g xs)
{- by definition of (.), fmap -}
== (f . g) x : (fmap f . fmap g) xs
{- by definition of (.) -}
== (f . g) x : fmap (f . g) xs
{- by inductive hypothesis -}Therefore, fmap (f . g) l == (fmap f . fmap g) l in all cases. ∎
Was it all for naught?
Turns out these instances of Functor implement fmap correctly. However, turns out proving the second law in any case is redundant due to the free theorem of fmap, but it was fun anyways.