[Haskell-cafe] Re: what is inverse of mzero and return?
Jules Bean
jules at jellybean.co.uk
Tue Jan 25 06:02:47 EST 2005
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
More information about the Haskell-Cafe
mailing list