[Haskell-cafe] Why Kleisli composition is not in the Monad signature?
AUGER Cédric
sedrikov at gmail.com
Tue Oct 16 16:37:15 CEST 2012
Le Tue, 16 Oct 2012 09:51:29 -0400,
Jake McArthur <jake.mcarthur at gmail.com> a écrit :
> On Mon, Oct 15, 2012 at 11:29 PM, Dan Doel <dan.doel at gmail.com> wrote:
> > I'd be down with putting join in the class, but that tends to not be
> > terribly important for most cases, either.
>
> Join is not the most important, but I do think it's often easier to
> define than bind. I often find myself implementing bind by explicitly
> using join.
join IS the most important from the categorical point of view.
In a way it is natural to define 'bind' from 'join', but in Haskell, it
is not always possible (see the Monad/Functor problem).
As I said, from the mathematical point of view, join (often noted μ in
category theory) is the (natural) transformation which with return (η
that I may have erroneously written ε in some previous mail) defines a
monad (and requires some additionnal law). As often some points it out,
Haskellers are not very right in their definition of Monad, not because
of the bind vs join (in fact in a Monad either of them can be defined
from the other one), but because of the functor status of a Monad. A
monad, should always be a functor (at least to fit its mathematical
definition). And this problem with the functor has probably lead to the
use of "bind" (which is polymorphic in two type variables) rather than
"join" (which has only one type variable, and thus is simpler).
The problem, is that when 'm' is a Haskell Monad which does not belong
to the Functor class, we cannot define 'bind' in general from 'join'.
That is in the context where you have:
return:∀ a. a → (m a)
join:∀ a. (m (m a)) → (m a)
x:m a
f:a → (m b)
you cannot define some term of type 'm b', since you would need to use
at the end, either 'f' (and you would require to produce a 'a' which
would be impossible), or 'return' (and you would need to produce a 'b',
which is impossible), or 'join' (and you would need to produce a 'm (m
b)', and recursively for that you cannot use return which would make
you go back to define a 'm b' term)
For that, you need the 'fmap' operation of the functor.
return:∀ a. a → (m a)
join:∀ a. (m (m a)) → (m a)
fmap:∀ a b. (a→b) → ((m a)→(m b))
x:m a
f:a → (m b)
in this context defining a term of type 'm b' is feasible (join (fmap f
x)), so that you can express "bind = \ x f -> join (fmap f x)".
To sum up, mathematical monads are defined from 'return' and 'join' as
a mathematical monad is always a functor (so 'fmap' is defined, and
'bind', which is more complex than 'join' can be defined from 'join'
and 'fmap'). Haskell does not use a very good definition for their
monads, as they may not be instance of the Functor class (although
most of them can easily be defined as such), and without this 'fmap',
'join' and 'return' would be pretty useless, as you wouldn't be able
to move from a type 'm a' to a type 'm b'.
More information about the Haskell-Cafe
mailing list