John Lato schrieb:
Hello,
I was wondering today, is this generally true?
instance (Monad m, Monoid a) => Monoid (m a) where mempty = return mempty mappend = liftM2 mappend
I know it isn't a good idea to use this instance, but assuming that the instance head does what I mean, is it valid? Or more generally is it true for applicative functors as well? I think it works for a few tricky monads, but that's not any sort of proof. I don't even know how to express what would need to be proven here.
I always assumed that 'm a' would be a monoid for 'm' being an applicative functor, but I never tried to prove it. Now you made me performing a proof. However the applicative functor laws from http://www.haskell.org/ghc/docs/6.12.2/html/libraries/base-4.2.0.1/Control-A... are quite unintuitive and the proofs are certainly not very illustrative. For the proof of the associativy I have just started from both ends and worked toward where the associativity of 'a' has to be inserted, added some mistakes and restarted. Left Identity ------------- (mappend mempty x :: m a) = liftA2 mappend (pure mempty) x = pure mappend <*> pure mempty <*> x = pure (mappend mempty) <*> x = pure id <*> x = x Right Identity -------------- (mappend x mempty :: m a) = liftA2 mappend x (pure mempty) = (pure mappend <*> x) <*> pure mempty = pure ($mempty) <*> (pure mappend <*> x) = pure (.) <*> pure ($mempty) <*> pure mappend <*> x = pure ((.) ($mempty)) <*> pure mappend <*> x = pure (($mempty).) <*> pure mappend <*> x = pure ((($mempty).) mappend) <*> x = pure (($mempty) . mappend) <*> x = pure (\a -> ($mempty) (mappend a)) <*> x = pure (\a -> (mappend a) mempty) <*> x = pure (\a -> a) <*> x = pure id <*> x = x For monads I find the proof more intuitive: liftM2 mappend x (pure mempty) = do y <- x z <- pure mempty return (mappend y z) = do y <- x return (mappend y mempty) = do y <- x return y = x Associativity ------------- ((x `mappend` y) `mappend` z) :: m a = (pure mappend <*> x <*> y) `mappend` z = pure mappend <*> (pure mappend <*> x <*> y) <*> z = pure (.) <*> pure mappend <*> (pure mappend <*> x) <*> y <*> z = pure (mappend.) <*> (pure mappend <*> x) <*> y <*> z = pure (.) <*> pure (mappend.) <*> pure mappend <*> x <*> y <*> z = pure ((mappend.).) <*> pure mappend <*> x <*> y <*> z = pure ((mappend.) . mappend) <*> x <*> y <*> z -- see proof below = pure (($mappend).((.).((.).mappend))) <*> x <*> y <*> z = pure (.) <*> pure ($mappend) <*> pure ((.).((.).mappend)) <*> x <*> y <*> z = pure ($mappend) <*> (pure ((.).((.).mappend)) <*> x) <*> y <*> z = pure ((.).((.).mappend)) <*> x <*> pure mappend <*> y <*> z = pure (.) <*> pure (.) <*> pure ((.).mappend) <*> x <*> pure mappend <*> y <*> z = pure (.) <*> (pure ((.).mappend) <*> x) <*> pure mappend <*> y <*> z = pure ((.).mappend) <*> x <*> (pure mappend <*> y) <*> z = pure (.) <*> pure (.) <*> pure mappend <*> x <*> (pure mappend <*> y) <*> z = pure (.) <*> (pure mappend <*> x) <*> (pure mappend <*> y) <*> z = (pure mappend <*> x) <*> ((pure mappend <*> y) <*> z) = pure mappend <*> x <*> (pure mappend <*> y <*> z) = x `mappend` (pure mappend <*> y <*> z) = x `mappend` (y `mappend` z) ((mappend.) . mappend) x y z = (mappend.) (mappend x) y z = (\f -> mappend.f) (mappend x) y z = (\f x -> mappend (f x)) (mappend x) y z = mappend (mappend x y) z -- Monoid associativity for type 'a' = mappend x (mappend y z) = (.) (mappend x) (mappend y) z = ((.).mappend) x (mappend y) z = (.) (((.).mappend) x) mappend y z = ((.).((.).mappend)) x mappend y z = ($mappend) (((.).((.).mappend)) x) y z = (($mappend).((.).((.).mappend))) x y z