Re: [Haskell-cafe] lawless instances of Functor

On Tue, Jan 5, 2010 at 8:15 AM, Dan Piponi wrote:

On Mon, Jan 4, 2010 at 3:01 PM, Derek Elkins wrote:

...

Ignoring bottoms the free theorem for fmap can be written:

If h . p = q . g then fmap h . fmap p = fmap q . fmap g

When I play with http://haskell.as9x.info/ft.html I get examples that look more like:

If fmap' has the same signature as the usual fmap for a type

and h . p = q . g

then fmap h . fmap' p = fmap' q . fmap g

From which it follows that if fmap' id = id then fmap' is fmap.

It should not be necessary to prove this as fmap has the appropriate type to be fmap' and therefore fmap' can simply be set to fmap.

But I don't know how to prove that uniformly for all types, just the ones I generated free theorems for.

Yes, I have the same problem. I generated a few examples using pretty much that site and generalized, but I haven't proven the general statement, though I'm pretty confident that it holds. Basically, I'm pretty sure the construction of that free theorem doesn't rely on any of the actual details of the type constructor and probably by using a higher-order notion of free theorem this could be formalized and then used to prove the above result. At this point, though, I haven't put much effort into proving that the free theorem holds uniformly (enough.)