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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
