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
> 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
```