[Haskell-cafe] lawless instances of Functor

[Paul Brauner]

Thanks. I was wondering if the free theorem of fmap entailed that
implication, but I'm not used enough to decipher the output of the tool,
neither am I able to generate it by hand.

However, if this holds (law1 => law2), I wonder why this isn't some
"classic" category theory result (maybe it is ?). I don't know much
about category theory, but it seems to me that functors are pretty
central to it. Maybe i'm confusing haskell's notion of Functor and
category theory functors.

Paul

On Tue, Jan 05, 2010 at 08:01:46AM +0900, Derek Elkins wrote:
> On Tue, Jan 5, 2010 at 7:14 AM, Paul Brauner <paul.brauner at loria.fr> wrote:
> > Hi,
> >
> > I'm trying to get a deep feeling of Functors (and then pointed Functors,
> > Applicative Functors, etc.). To this end, I try to find lawless
> > instances of Functor that satisfy one law but not the other.
> >
> > I've found one instance that satisfies fmap (f.g) = fmap f . fmap g
> > but not fmap id = id:
> >
> > data Foo a = A | B
> >
> > instance Functor Foo where
> >  fmap f A = B
> >  fmap f B = B
> >
> > -- violates law 1
> > fmap id A = B
> >
> > -- respects law 2
> > fmap (f . g) A = (fmap f . fmap g) A = B
> > fmap (f . g) B = (fmap f . fmap g) B = B
> >
> > But I can't come up with an example that satifies law 1 and not law 2.
> > I'm beginning to think this isn't possible but I didn't read anything
> > saying so, neither do I manage to prove it.
> >
> > I'm sure someone knows :)
> 
> Ignoring bottoms the free theorem for fmap can be written:
> 
> If h . p = q . g then fmap h . fmap p = fmap q . fmap g
> Setting p = id gives
> h . id = h = q . g && fmap h . fmap id = fmap q . fmap g
> Using fmap id = id and h = q . g we get,
> fmap h . fmap id = fmap h . id = fmap h = fmap (q . g) = fmap q . fmap g
> 
> So without doing funky stuff involving bottoms and/or seq, I believe
> that fmap id = id implies the other functor law (in this case, not in
> the case of the general categorical notion of functor.)