[Haskell-cafe] lawless instances of Functor

[Derek Elkins]

On Tue, Jan 5, 2010 at 8:15 AM, Dan Piponi <dpiponi at gmail.com> wrote:
> On Mon, Jan 4, 2010 at 3:01 PM, Derek Elkins <derek.a.elkins at gmail.com> 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.)