My category theory is pretty weak, but I'll take a stab (others can
correct me if I say something stupid):
ok wrote:
It is considerably more than a little revisionist to identify Haskell
monads with Category Theory monads.
Quoting the Wikipedia article on monads:
"If F and G are a pair of adjoint functors, with F left adjoint to G,
then the composition G o F will be a monad.
Note that therefore a monad is a functor from a category to itself;
and that if F and G were actually inverses as functors the corresponding
monad would be the identity functor."
So a category theory monad is a functor from some category to itself.
How is IO a a functor?
It is an endofunctor in the category whose objects are Haskell types and
whose arrows are Haskell functions.
Which category does it operate on? What does it
do to the points of that category? What does it do to the arrows?
It maps objects (Haskell types) to boxed types (Haskell monads), i.e.
sets of values of a certain type to sets of computations resulting in a
value of that type.
It maps arrows (Haskell functions) to Kleisli arrows, i.e. it maps the
set of functions {f : a -> b} into the set of functions {f : a -> m b}.
Let's turn to the formal definition:
"If C is a category, a monad on C consists of a functor T : C → C
together with two natural transformations: η : 1 → T (where 1
denotes the identity functor on C) and μ : T2 → T (where T2 is
the functor T o T from C to C). These are required to fulfill
[some] axioms:"
What are the natural transformations for the IO monad?
η is the unit Kleisli arrow:
return :: (Monad m) => a -> m a
μ : T2 → T is the join function
join :: (Monad m) => m (m a) -> m a
I suppose there
is a vague parallel to return and >>=, but that's about all you can claim
for it.
There is more than a vague claim. From
http://www.haskell.org/haskellwiki/Monads_as_containers:
(>>=) :: (Monad m) => m a -> (a -> m b) -> m b
xs >>= f = join (fmap f xs)
join :: (Monad m) => m (m a) -> m a
join xss = xss >>= id
If we are not to be revisionist, then we must admit that Haskell monads
were *inspired* by category theory monads, but went through a couple of
rounds of change of notation before becoming the Monad class we know and
love today.
Apparently only some of use love Haskell monads! :) The notation seems
like a pretty straightforward mapping to me.
What we have *was* invented for functional programming and
its category theory roots are not only useless to most programmers but
quite unintelligible.
I would say "applied" rather than "invented". Clearly "useless" and
"unintelligible" are predicates of the programmer.
> We cannot (and I do not) expect our students to
*care* about monads because of their inspiration in category theory but
because they WORK for a problem that had been plaguing the functional
programming community for a long time.
Maybe you should raise your expectations?
This is why I say you must consider your audience.
On second thought, maybe I should have considered my audience before
replying to your email. The prior probability of persuasion occurring is
maybe somewhat small, but I'm a sucker for lost causes...
Dan Weston
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
