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

[Jules Bean]

On 25 Jan 2005, at 10:32, Keean Schupke wrote:

> I think I see, but if the objects are types, arn't the morphisms 
> functions
> on types not values?
>

No. Well: they are functions 'on' types, but functions 'on' types map 
values to values.

Analogy: In the category of sets and functions, the objects are sets 
and the morphisms are functions. The functions --- from sets to sets 
--- take objects in one set to objects in another set.

Specifically:

A monad T is a (endo)functor T : * -> * where * is the category of 
types, together with a multiplication mu and a unit eta.

mu is a natural transformation between the functor TT and the functor T.
eta is a natural transformation between the identity functor iota and 
the functor T.

A natural transformation is defined as a (natural) family of morphisms, 
so mu is defined by a family of functions

mu_a : T T a -> T a

That is, for every type 'a' there is an ordinary function mu_a of type 
T T a -> T a. In particular, for a == Int, there is a function mu_Int : 
T T Int -> T Int.

For T as the list monad [], mu_Int is concat : [[Int]] -> [Int]
For T as the IO monad, mu_Int is the function IO IO Int -> IO Int given 
by 'the action which consists of doing all the actions from the outer 
IO followed by all the actions from the inner IO'

Similarly, eta_Int : Int -> [Int] is (\x -> [x]), eta_IO : Int -> IO 
Int is 'the action which does nothing and then returns x'

Then the monad laws (associativity for mu, and left/right unit laws for 
eta over mu) must hold for all types. At each type, they refer to 
equality on functions, which is defined pointwise, so they must be 
equal at all values.

Jules