Re: [Haskell-cafe] monoids and monads
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) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] monoids and monads
On Tue, Jul 27, 2010 at 8:32 AM, Henning Thielemann schlepp...@henning-thielemann.de wrote: 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 Thanks very much, this is what I was unable to express properly (hence the informal description). 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) So the task now is to prove that these laws hold, given the instance I defined above, the monoid laws for 'a', and the monad laws for 'm'. Or alternatively using applicative laws for 'm' for the more general case. I'll see how I get on from here then. Thanks, John ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] monoids and monads
On Mon, Jul 26, 2010 at 5:02 PM, Edward Kmett ekm...@gmail.com wrote: On Mon, Jul 26, 2010 at 11:55 AM, John Lato jwl...@gmail.com 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 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-Monoid-Monad.html I think your monoids package has grown since I last looked at it. I'll take a look. 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. Thanks very much. With this and Henning's hints, I think I can make some progress with this now. John ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] monoids and monads
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] monoids and monads
On Tuesday 27 July 2010 8:50:56 am Henning Thielemann wrote: 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. Perhaps a clearer approach is to look at the category theory behind this. First, a monoid object in a monoidal category (C, I, ⊗) consists of An object M e : I - M m : M ⊗ M - M satisfying unit and associativity diagrams. Second, a lax monoidal functor F between two monoidal categories C and D gets you: unit : I_D - F I_C pair : FA ⊗_D FB - F(A ⊗_C B) also satisfying unit and associativity diagrams. We're only dealing with endofunctors, so the above simplifies to: unit : I - F I pair : forall A B. F A ⊗ F B - F(A ⊗ B) and in the Haskell case, you get applicative functors via: pure x = fmap (const x) unit f * x = fmap (uncurry ($)) (pair (f, x)) So, if we have a monoid object M and monoidal functor F, then we have: Fe . unit : I - FM Fm . pair : FM ⊗ FM - FM which should be suggestive. From there, the unit and associativity laws for FM as a monoid object should follow pretty naturally using laws of the parts. For instance... I ⊗ FM - FI ⊗ FM - FM ⊗ FM - F(M ⊗ M) - FM is the same as I ⊗ FM - FM via the isomorphism for the monoidal category 1) We know that I ⊗ FM - FI ⊗ FM - F(I ⊗ M) - FM is the same as I ⊗ FM - FM from F's left-identity coherence law 2) We know that I ⊗ M - M ⊗ M - M is the same as I ⊗ M - M from M's left-identity law, and thus F(I ⊗ M) - F(M ⊗ M) - FM is the same as F(I ⊗ M) - FM from F being a functor. 3) Finally, we know that FI ⊗ FM - FM ⊗ FM - F(M ⊗ M) is the same as FI ⊗ FM - F(I ⊗ M) - F(M ⊗ M) because 'pair' is supposed to be natural in A and B. So: I ⊗ FM - FM is the same as (1) I ⊗ FM - FI ⊗ FM - [F(I ⊗ M) - FM] is the same as (2) I ⊗ FM - [FI ⊗ FM - F(I ⊗ M) - F(M ⊗ M)] - FM is the same as (3) I ⊗ FM - FI ⊗ FM - FM ⊗ FM - F(M ⊗ M) - FM which is left-identity. Right-identity is exactly the same proof with objects reflected around the ⊗. Associativity of the monoid should be a similar application of the associativity laws, plus functor and naturality identities. You could also couch these in terms of Haskell if preferred: unit :: f () pair :: (f a, f b) - f (a, b) assoc (x, (y, z)) = ((x, y), z) fmap (f *** g) . pair = pair . (fmap f *** fmap g) fmap assoc . pair . (id *** pair) = pair . (pair *** id) . assoc etc. Alternately, if you accept authority: Lax monoidal functors send monoids to monoids http://ncatlab.org/nlab/show/monoidal+functor -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] monoids and monads
Henning Thielemann wrote:
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.
I always found it more illustrative to break it down and talk about
pointed functors, where 'return' is trivial in 'fmap' (forgive the Coq
syntax):
fmap_pointed
: forall {A B : Type} (f : A - B) (a : A)
, f $ return a = return $ f a
And then you only need three laws, the obvious ones:
app_return_left
: forall {A B : Type} (f : A - B) (xa : F A)
, return f * xa = f $ xa
app_return_right
: forall {A B : Type} (xf : F (A - B)) (a : A)
, xf * return a = ($a) $ xf
app_compose
: forall {A B C : Type}
, forall (xf : F (B - C)) (xg : F (A - B)) (xa : F A)
, compose $ xf * xg * xa = xf * (xg * xa)
That is, we have that 'return' is (in the appropriate sense) the left
and right identity for (*), which allows us to apply fmap_pointed to
reduce (*) into ($). Since only one of the arguments has a
non-trivial structure, that's the structure we use for ($).
And then we have (again in the appropriate sense) associativity of
composition. Which is really just to say that composition from the pure
world is preserved as composition in the applicative world.
The other two laws (app_identity : ..., return id $ xa = xa) and
(app_homomorphism : ..., return f * return a = return (f a)) follow
directly from fmap_pointed. Or conversely, given these five laws we can
always prove fmap_pointed.
--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] monoids and monads
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. Any resources for how I could develop a means to reason about this sort of property? Thanks, John ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] monoids and monads
On Mon, Jul 26, 2010 at 11:55 AM, John Lato jwl...@gmail.com 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-Monoid-Monad.html 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Monoids [Stacking monads]
Ryan Ingram wrote: Newtypes is the general ( sadly unsatisfactory) answer: Oh dear. Well that _is_ pretty unsatisfactory... Given the constraints of the Haskell type system, could we do better in principle? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
