Functor laws and natural transformations in Haskell
I'm having a little trouble exactly what question you're asking, but I think it might help if we went through the connection between homomorphisms and free theorems.

But here's the executive summary of what I think you want to know:


The fmap laws are not redundant when you have free theorems. On the contrary, you need fmap to state the free theorem for any function that involves a Haskell Functor.
Specifically, if a function has the type of a natural transformation, its free theorem is the naturality condition expressed in terms of fmap.


First off, let's get a bit of intuition about what the parametricity theorem states. An informal way of stating it is this: For any function which has a "forall" in its type, that "forall" really does mean "for all types". The function cannot make any assumptions whatsoever about the type.

To explain what this means when we involve types with an algebra, we need the language of homomorphisms. So let's review what a homomorphism is. (Sorry if this is revision for you, but I think it's worth going through this.)

Let's consider monoids. A monoid is a set $M$ along with two operations $0_M$ and $+_M$ which obeys the laws:

$$\forall x \in M, x +_M 0_M = 0_M +_M x = x$$
$$\forall x,y,z \in M, x +_M (y +_M z) = (x +_M y) +_M z$$

A monoid homomorphism is a function between two monoids $f : M \rightarrow N$ which "respects" the two operations:

$$f(0_M) = 0_M$$
$$f(x +_M y) = f(x) +_N f(y)$$

In Haskell, we might represent monoids as a type class:

class Monoid m where
    mzero :: m
    mplus :: m -&gt; m -&gt; m


If M1 and M2 are instances of Monoid, a Monoid homomorphism f :: M1 -&gt; M2 must obey the laws:

f mzero = mzero
f (mplus x y) = mplus (f x) (f y)


Remember that the monoid operations on the left-hand side of these "laws" are different from the monoid operations on the right-hand side. The left-hand side are the operations for M1 and the right-hand side are the operations for M2.

Now consider the following typeclass (which isn't the same as Haskell's Ord typeclass, but is close enough):

class Ordered a where
    lessThan :: a -&gt; a -&gt; Bool


Again, there are laws that any reasonable "less than" operator must obey. But what I want to concentrate on here is the Bool part.

What does it mean for a function to "respect" this algebra? It essentially means that the Bool has to be the same. That is, if A and B are both instances of Ordered, an Ordered homomorphism f :: A -&gt; B must obey the law:

lessThan (f x) (f y) = lessThan x y


Think about what this means semantically: this law is stating that for any two elements, f doesn't change their relative ordering. That is what it means for f to "respect" the ordering algebra.

OK, now back to the parametricity theorem. The free theorem for the function:

sortBy :: forall a. (a -&gt; a -&gt; Bool) -&gt; [a] -&gt; [a]


is this, written out in a slightly fuller form:

for all f :: A -&gt; B,
If lt :: A -&gt; A -&gt; Bool is a function such that
    for all x, y :: A, lt x y = lt (f x) (f y)
Then
    for all xs :: [A], sortBy lt . map f = map f . sortBy lt


We can say the same thing with type classes:

sort :: forall a. Ordered a =&gt; [a] -&gt; [a]


The free theorem here is, essentially:

for all f :: A -&gt; B,
if f is an Ordered homomorphism
then sort . map f = map f . sort


Which is, of course, just that f doesn't change the ordering of elements, then performing the substitution map f and then sorting is the same thing as sorting them performing the substitution.

The complication with Functor is that it's a constructor class, so the intuition about what a Functor homomorphism should be is a little less clear. But let's step back a moment and talk about category homomorphisms.

Categories are algebras just like any other. A category has two operations, $1$ and $\circ$, which satisfies the laws that you know and love. So a category homomorphism $F$ is a function which satisfies:

$$F(\hbox{id}) = \hbox{id}$$
$$F(g \circ f) = F(g) \circ F(f)$$

If you think of a functor between the "Haskell category" (objects are Haskell types, morphisms are Haskell functions) and a Haskell Functor category (objects are Haskell functors and morphisms are Haskell functions between these objects), then this is exactly the Functor laws.

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


Now here's the important part: The fmap operation is the homomorphism precondition that you need for free theorems involving Functor.

Consider, for example, something with the same type as fmap but isn't necessarily fmap:

instance Functor F where ...

somethingLikeFmap :: forall a b. (a -&gt; b) -&gt; (F a -&gt; F b)


The free theorem for this function is:

if q . f = g . p,
then somethingLikeFmap q . fmap f = fmap g . somethingLikeFmap p


From this you can conclude a bunch of interesting things, such as that if somethingLikeFmap id = id then fmap = somethingLikeFmap. In particular, somethingLikeFmap can be characterised entirely by what it does with id.

This has to be the case. The parametricity theorem, which generates these free theorems, states the "forall" in a parametric type really does mean "for all types".

If the functor is a container-like type, for example, the function cannot make any decision about what to do based on the value of an element in the container. But it could do anything with the structure of the container which doesn't depend on the values in it.

somethingLikeMap1 f = reverse . map f
somethingLikeMap2 f = map f . tail
somethingLikeMap3 f = []


If a polymorphic function does has a way to make decisions based on the values (e.g. lessThan in the case of sort), then the free theorem states that this is the only way that it can make a decision about what to do, so if the mapping doesn't affect the decisions (e.g. the values returned by lessThan), then it doesn't affect the operation of the polymorphic function (e.g what sort does).

So this is why the fmap laws are not redundant with respect to free theorems: they define the homomorphism between the Haskell category and the (endo-) functor category that you need to state the free theorems.

Finally, what is the free theorem of a function which has the type of a natural transformation?

instance Functor F where ...
instance Functor G where ...

eta :: forall a. F a -&gt; G a


It is:

fmap_G f . eta = eta . fmap_F f


This is exactly the naturality condition. This a good way to think about what's so "natural" about a natural transformation.