Remove warning from the second functor law article

[duplode]

I am convinced that you don't need to worry about the claim of circularity you mention at the top of the second law article, and I think I can explain why. In your article, you quote the free theorem as:

        f .      g =      p .      q -- (1) Given this ...
=> fmap f . fmap g = fmap p . fmap q -- (2) ... this holds

The Kmett article you mention in the warning, however, gives it as...

The free theorem for fmap :: (a -> b) -> F a -> F b is that given functions f, g, k, and h such that

g . h = k . f

then

$map g . fmap h = fmap k . $map f

where $map is the "natural map" for the type constructor F.

... and then goes on to prove that fmap f = $map f (that is the Lemma 1 there), which leads to the free theorem as you quoted it. Now, I think it is fine to skip this preliminary step in your article, as it would make the discussion more complicated than it needs to be. I am only mentioning it because it is likely that the objection to the proof was raised because of a misunderstanding of that original form of the free theorem.

The whole issue, as I understand it, hinges on that fmap and $map play different roles in the free theorem: fmap is the function you are proving something about, while $map is just part of the free theorem generating machinery. Still, fmap f = $map f, and so whoever complained about the proof probably thought: "Wait a minute -- you are proving a theorem about fmap which machinery that uses fmap. That's circularity!" That, however, would be a misunderstanding: $map does not presuppose that a Functor is involved. Nor, by the way, is using it "a bit hand-wavy", something Edward worries about in the conclusion of his article. $map is perfectly well-defined, albeit implicitly, in section 2 of Theorems for Free!. It is simply what you get when you consider a type polymorphic at a single (covariant) position and restrict the type-defining relation being specified there to a function -- in fact, Wadler even makes an aside about how, for lists, in that case the relation happens to be "the familiar 'map' function". To frame it in another way, the procedure for generating $map for a type is essentially the same thing that GHC does when you use DeriveFunctor: a mechanical procedure, which presupposes nothing other than the "shape" of the type... and which happens to produce fmap thanks to category theoretical reasons.

All things considered, I believe you can safely remove the warning at the top of the article. It would be nice to retain the link to Kmett's article, though, perhaps alongside the other ones at the bottom of the article.

[quchen]

Thanks for the long comment! It’s always good to see people are still reading my articles, and even better when they find helpful comments or things worth updating in them! :-)