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