[Haskell-cafe] monoids and monads

[wren ng thornton]

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