[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