[Haskell-cafe] Re: what is inverse of mzero and return?

[Jules Bean]

On 25 Jan 2005, at 11:56, Keean Schupke wrote:

> I guess I am trying to understand how the Monad laws are derived from 
> category theory...
> I can only find referneces to associativity being required.

Associativity and left and right unit laws.

> Monads are defined on functors, so the associativity just requires the 
> associativity of the
> 'product' operation on functors...
>
> I guess I don't quite see how associativity of functors (of the 
> category of functions on types) implies identity on values... surely 
> just the identity on those functors is required?
>

The 'associativity' isn't actually saying that the functors are 
associative. (Functorial composition is of course associativity, that's 
a fundamental fact about category theory). The 'associativity' is 
saying that the 'operation' given by the 'multiplication' 
transformation mu is 'associative'.

The proliferation of scare quotes is because monad are not monoids. 
They are a slightly different notion, but the analogy with monoids is 
strong, and the words used (multiplication, left and right units, 
associativity) are borrowed from the words used to talk about monoids.

The associativity law says that, given mu : T T -> T (a natural 
transformation), there are two possible ways of going from T T T -> T 
using mu, as in (T T) T -mu-> T T -mu-> T    and   T (T T) -mu-> T T 
-mu-> T.

We require that these two ways be equal as natural transformations. A 
natural transformation is a natural family of morphisms, and for two 
natural transformations to be equal, each morphism must be equal. A 
morphism in this case is a haskell function, and for two morphisms to 
be equal they must agree on every value.

The concrete example for [] is:

concat . (map concat)
should be the same (on all values of all types [a]) as
concat . concat

If it helps, the unit laws are that these two functions:

Prelude> :t (\x -> concat [x])
(\x -> concat [x]) :: forall a. [a] -> [a]
Prelude> :t concat . (\x -> [x])
concat . (\x -> [x]) :: forall a. [a] -> [a]

Are both equal (pointwise) to id : [a] -> [a]

Jules