
On Tue, 2010-01-05 at 08:01 +0900, Derek Elkins wrote:
On Tue, Jan 5, 2010 at 7:14 AM, Paul Brauner
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.