[Haskell-cafe] monoids and monads

[Dan Doel]

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