RE [Haskell-cafe] Monad Description For Imperative
Dan Weston
westondan at imageworks.com
Thu Aug 2 19:51:00 EDT 2007
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
More information about the Haskell-Cafe
mailing list