[Haskell-cafe] Re: lawless instances of Functor

Maciej Piechotka uzytkownik2 at gmail.com
Mon Jan 4 21:25:22 EST 2010


On Tue, 2010-01-05 at 08:01 +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.)

Hmm. Not quite a proff as we want to use: For all f g fmap (f . g) =
fmap f . fmap g. So we need to operate on arbitrary f and g. Also in
first line conclusion is used - at this stage we don't know if h . p =
p . q -> fmap h . fmap p = fmap q . fmap g.


Especially that (A->B) functions is |A|^|B| (and in haskell |A| >= 1, |
B| >= 1). Now imagine that (in pseudocode[1]):
rho :: (A -> B) -> A -> B
rho f | f is A -> A = id
      | f is Integral -> Integral = (+1) . fromIntegral
      | otherise = f

then

instance Functor Foo where
  fmap f (Something a) = Something $ rho f a

then

fmap id = id
but
if f = (+1) . fromIntegral :: Integer -> Int
   g = (-1) . fromIntegral :: Int -> Integer
then

fmap (f . g) = fmap id
but
fmap f . fmap g = fmap (+2)

Regards

[1] It can nearly be written in Haskell+Rules but rules does not have
precedence.




More information about the Haskell-Cafe mailing list