Do the functor laws prove complete preservation of

问题:

In the documenation for Data.Functor the following two are stated as the functor laws, which all functors should adhere to.

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

The way my intuition tells me functors should work is that they should be "structure preserving", or in other words, if you have a function f :: a -> b and it's inverse g :: b -> a then

fmap f . fmap g  ==  id

I have not been able to come up with an implementation of fmap that would adhere to the first two laws and violate the second, but that's hardly proof. Can someone enlighten me?

回答1:

Actually, your "third" functor law follows directly from actual functor laws and the fact that f . g ≡ id:

fmap f . fmap g ≡ fmap (f . g) ≡ fmap id ≡ id

And there's more: Haskell ensures that if first law holds for Functor instance, then the second one also holds (this is a free theorem for the type of fmap). I.e. you have to prove only fmap id ≡ id law for your Functor instance to ensure that it is valid.