RE [Haskell-cafe] Monad Description For Imperative

[Dan Weston]

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