[Haskell-cafe] monoids and monads

[Henning Thielemann]

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-Applicative.html
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