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