`The second Functor law is redundant` is not proper about articles HOT 3 CLOSED

Regarding your second point, f doesn't have the type [a] -> [a], it has the type (Num a, Ord a) => [a] -> [a]. All functions with the type forall a. [a] -> [a] have the stated property.

The reason this property holds is that a function with the type forall a. [a] -> [a] cannot examine the items in the list (it must work for all types a). As a result, the list it gives back can only contain items from the list given to it (although the list structure can be different, it cannot have different items or make choices about the list structure based on the specific properties of any of the items).

That property of map is the free theorem of map. The breakthrough paper on free theorems is Philip Wadler's Theorems for free! (although it uses somewhat outdated notation by today's standards). This particular property of map is described in the first part of the introduction and section 3.5 elaborates on the usefulness of using that property to think about map.

from articles.

For the first point, we can use the free theorem (this is a key part of the proof):

        f .      g =      p .      q
=> fmap f . fmap g = fmap p . fmap q

This lets us turn any equation of the form f . g = p . q into an equation fmap f . fmap g = fmap p . fmap q.

For the precondition in that implication, first we note that this equation holds

        f .      g =      (f . g) .      id

Then we let p = (f . g) and q = id, plug this into the free theorem and end up with

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

This can be simplified, using fmap id = id to

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

and simplified again using the identity law h . id = h, to

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

(This is the same proof as the one in the article, worded in a slightly different way.)

from articles.

Thanks @roboguy13 for answering :-)

5dd82fe adds a short remark in order to clarify the first question.

from articles.