On Mon, Jul 26, 2010 at 11:55 AM, John Lato wrote:

Hello,

I was wondering today, is this generally true?

instance (Monad m, Monoid a) => Monoid (m a) where mempty = return mempty mappend = liftM2 mappend

Yes.

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.

There are multiple potential monoids that you may be interested in here. There is the monoid formed by MonadPlus, there is the monoid formed by wrapping a monad (or applicative) around a monoid, which usually forms part of a right seminearring because of the left-distributive law, there are also potentially other monoids for particular monads. See the monad module in my monoids package: http://hackage.haskell.org/packages/archive/monoids/0.2.0.2/doc/html/Data-Mo...

Any resources for how I could develop a means to reason about this sort of property?

The types are not enough. What you need is the associativity of Kleisli arrow composition and the two identity laws. The three monad laws are precisely what you need to form this monoid. There are analogous laws for Applicative that serve the same purpose. -Edward Kmett

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 translate 'valid' and 'true' to "Is 'm a' a Monoid, given that 'm' is a Monad and 'a' is a Monoid?" If this is the question then we have to show the Monoid laws for (m a), namely left identity: forall x. mappend mempty x = x right identity: forall x. mappend x mempty = x associativity: forall x y z. (x `mappend` y) `mappend` z = x `mappend` (y `mappend` z)

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