Do the functor laws prove complete preservation of structure?
category-theory, functional-programming, haskell
Solution
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.
Problem
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?