[Haskell-cafe] monoids and monads
Dan Doel
dan.doel at gmail.com
Tue Jul 27 10:37:34 EDT 2010
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
More information about the Haskell-Cafe
mailing list