second_functor_law.md

Warning. I've temporarily taken down this article in the past due to a rumor I've heard about its subject, so I wasn't sure anymore whether the main claim is correct.

That claim is that in order to derive the free theorem of fmap, one has to have a functor in the first place, so both the first and second law are already given. Under those circumstances, deriving the second from the first law would be proving one of the premises that lead to it.

I have not been able to confirm my doubts. However, there is another article by the much more knowledgeable Edward Kmett which makes the same claim as you can find below, hinting that I might be correct, albeit without knowing exactly why.

Make of this what you want. Here's the former article:

The second Functor law is redundant

Basic Haskell teaches that instances of Functor should satisfy

fmap id = id                   -- fmap preserves identity
fmap f . fmap g = fmap (f . g) -- fmap distributes over composition

However, Haskell's type system is special in a way that makes the second law follow from the first one. The values of every type follow a certain law; this law is called the free theorem of that type. For example, the free theorem of f :: [a] -> [a] is

map g . f  = f . map g

This means that any function f of type [a] -> [a] commutes with map; for example one can choose f = reverse, and then the law reads

map g . reverse = reverse . map g

This holds for all g; so from the type of f alone, one can deduce that we can rearrange it in a chain of maps to be in any place we want. Pretty cool how something like that can be derived from a type alone!

Similarly, you can generate the free theorem for fmap, which reads

        f .      g =      p .      q -- (1) Given this ...
=> fmap f . fmap g = fmap p . fmap q -- (2) ... this holds

In other words, this says that whenever functions compose, fmapping all of them still composes.

Now choose p = id and q = f . g in (2),

  fmap f . fmap g
= fmap id . fmap (f . g)
= id . fmap (f . g)      -- by the first functor law
= fmap (f . g)

This is precisely the second Functor law,

fmap f . fmap g = fmap (f . g)

Note how we used nothing but fmap's type (to generate the free theorem) and the first Functor law (to eliminate fmap id) to derive this. It is worth mentioning that this only holds up to fast and loose reasoning, i.e. assuming no ⊥ are involved, otherwise e.g.

newtype Id a = Id a

instance Functor Id where
      fmap f x = f `seq` x `seq` (Id . f . runId) x

satisfies the first, but not the second, Functor law:

fmap id x = id `seq` x `seq` (Id . id . runId) x
          = id `seq` (x `seq` (Id . id . runId) x) -- seq is infixr 0
          = x `seq` (Id . runId) x
          = x `seq` x
          = x

-- but
(fmap (const ()) . fmap ⊥) x
      = fmap (const ()) (fmap ⊥ x)
      = fmap (const ()) (⊥ `seq` <stuff>)
      = fmap (const ()) ⊥
      = <stuff> `seq` ⊥ `seq` ...
      = ⊥
fmap (const () . ⊥) x
      = (const () . ⊥) `seq` x `seq` (Id . (const ()) . ⊥) . runId) x
      = const () . ⊥ `seq` (x `seq` (Id . const () . ⊥ . runId) x)
      = x `seq` (Id . const () . ⊥ . runId) x
      = x `seq` Id (const () (⊥ (runId x)))
      = x `seq` Id ()
      -- This is ⊥ if and only if x is ⊥.

If you want to know more about free theorems or just play around with them:

• Online free theorem generator (make sure to "hide type instantiations"; the free theorem is displayed in the very last box in a somewhat readable format)
• Theorems for free!, the original publication on free theorems