Haskell Functor implied law

问题:

Typeclassopedia says:

"A similar argument also shows that any Functor instance satisfying the first law (fmap id = id) will automatically satisfy the second law as well. Practically, this means that only the first law needs to be checked (usually by a very straightforward induction) to ensure that a Functor instance is valid."

If this is the case, why do we even mention the second functor law?

Law 1: fmap id = id
Law 2: fmap (g . h) = (fmap g) . (fmap h)

回答1:

While I can't give a proof, I believe what this is saying is that due to parametricity, the type system enforces the second law as long as the first law holds. The reason to specify both rules is that in the more general mathematical setting, you might have some category C where it is perfectly possible to define a "mapping" from C to itself (i.e. a pair of endofunctions on Obj(C) and Hom(C) respectively) which obeys the first rule but fails to obey the second rule, and therefore fails to constitute a functor.

Remember that Functors in Haskell are endofunctors on the category Hask, and not even everything that would mathematically be considered an endofunctor on Hask can be expressed in Haskell... the constraints of parametric polymorphism rule out being able to specify a functor which does not behave uniformly for all objects (types) which it maps.

Based on this thread, the general consensus seems to be that the second law follows from the first for Haskell Functor instances. Edward Kmett says,

Given fmap id = id, fmap (f . g) = fmap f . fmap g follows from the free theorem for fmap.

This was published as an aside in a paper a long time back, but I forget where.

回答2:

Using seq, we can write an instance which satisfies the first rule but not the second one.

data Foo a = Foo a
    deriving Show

instance Functor Foo where
    fmap f (Foo x) = f `seq` Foo (f x)

We can verify that this satisfies the first law:

fmap id (Foo x)
= id `seq` Foo (id x)
= Foo (id x)
= Foo x

However, it breaks the second law:

> fmap (const 42 . undefined) $ Foo 3
Foo 42
> fmap (const 42) . fmap undefined $ Foo 3
*** Exception: Prelude.undefined

That said, we usually ignore such pathological cases.

回答3:

I'd say the second law is not mentioned for validity reasons, but rather as an important property:

The first law says that mapping the identity function over every item in a container has no effect. The second says that mapping a composition of two functions over every item in a container is the same as first mapping one function, and then mapping the other. --- Typeclassopedia

(I can't see why this first law implies the second law, but I'm not a skilled Haskeller - its probably obvious when you know what's going on)

回答4:

It seems that it was realized quite recently that law 2 follows from law 1. Thus, when the documentation was originally written, it was probably thought to be an independent requirement.

(Personally, I'm not convinced by the argument, but since I haven't had the time to work out the details myself, I'm giving it the benefit of doubt here.)