[Haskell-cafe] monoids and monads
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
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
More information about the Haskell-Cafe
mailing list