[Haskell-cafe] Why Kleisli composition is not in the Monad signature?

Kim-Ee Yeoh ky3 at atamo.com
Wed Oct 24 07:36:52 CEST 2012


On Tue, Oct 16, 2012 at 9:37 PM, AUGER Cédric <sedrikov at gmail.com> wrote:

> 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).


Auger:

Your emails keep invoking "the mathematical point of view" as if it were
something unique and universal.

Mathematical definitions are created and adopted to the extent that they
give rise to interesting, meaningful proofs. Coding in Haskell is precisely
proving theorems in a branch of constructive mathematics. Its practitioners
have found one set of monad definitions more intuitive and sensible when
working on such proofs than another such set.

I don't understand your dogmatism about return and join being canonically
the best monad definition in all possible mathematics. That's truly a
quantifier that beggars imagination.

-- Kim-Ee


On Tue, Oct 16, 2012 at 9:37 PM, AUGER Cédric <sedrikov at gmail.com> wrote:

> 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'.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121024/73147978/attachment.htm>


More information about the Haskell-Cafe mailing list