Henning Thielemann schlepptop at henning-thielemann.de
Tue Jul 27 08:50:56 EDT 2010

```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
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

```