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

[AUGER Cédric]

Le Tue, 16 Oct 2012 11:58:44 -0400,
Dan Doel <dan.doel at gmail.com> a écrit :

> On Tue, Oct 16, 2012 at 10:37 AM, AUGER Cédric <sedrikov at gmail.com>
> wrote:
> > 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).
> 
> This is the way it's typically presented. Can you demonstrate that it
> is the most important presentation?

What do you mean by demonstrate? If you do not want to fit the
mathematical presentation, then I have nothing to demonstrate, you have
your point of view, I have mine and they differ. Now, if you want to
fit the mathematical presentation, then a monad is an endofunctor with
two natural transformations (η=return and μ=join) satisfying some laws.
(when I write 'natural' I mean the mathematical definition of natural,
not its common definition as something on which we think immediately,
or something which is obvious).
A natural transformation from S to T (where S and T are functors from a
category C to a category D) is for each object 'x' of C, a morphism
from S x to T x satisfying some property.

return is a natural transformation from the "Id" functor to the "M"
functor (where M is the monad), while join is a natural transformation
from the "MM" functor to the "M" functor.

If you want to express bind, that would be a natural transformation
from a functor F to a functor G from "C*×C" (where C* is the opposite
category of C) to the "(Id↓M)" comma-category.

F would be defined as (a,b)↦Hom(a, M b)
    φ:Hom(a',a)×ψ:Hom(b,b')↦λ (f:Hom(a,M b)). (M ψ)∘f∘φ
while G would be defined as (a,b)↦Hom(M a, M b)
    φ:Hom(a',a)×ψ:Hom(b,b')↦λ (f:Hom(M a, M b)). (M ψ)∘f∘(M φ)

well, I guess it would be possible to define a monad with 'bind' as a
natural transformation, but how complex it would be where 'join' is so
simple. Plus 'return' and 'join' can be nicely composed to get the
monad laws.

> I'd urge caution in doing so, too. For instance, there is a paper,
> Monads Need Not Be Endofunctors, that describes a generalization of
> monads to monads relative to another functor.

Yes, so these are not monads. Your paper being written on 15 pages is
some indication that it is more complex than simple monads.

I will take a look on your relative adjunctions to understand what it
exactly is.

> And there, bind is
> necessarily primary, because join isn't even well typed. I don't think
> it's written by mathematicians per se (rather, computer
> scientists/type theorists). But mathematicians have their own
> particular interests that affect the way they frame things, and that
> doesn't mean those ways are better for everyone.

Once again, I never said that Monads with 'join' rather than 'bind'
are better in all points. I only said that it better fits the
mathematical point of view. Also note, that there is no true wall
between sciences. Lot of things being interesting in some scientific
domain can also be seen as interesting in some other scientific domain.

> 
> > 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'.
> 
> I don't think Functor being a superclass of Monad would make much
> difference. For instance, Applicative is properly a subclass of
> Functor, but we don't use the minimal definition that cannot reproduce
> fmap on its own:
> 
>     class Functor f => LaxMonoidal f where
>       unit :: f ()
>       pair :: f a -> f b -> f (a, b)
> 
> Instead we use a formulation that subsumes fmap:
> 
>     fmap f x = pure f <*> x
> 

My background on that matter is not strong enough to discuss that
point, I never used that stuff.

> Because those primitives are what we actually want to use, and it's
> more efficient to implement those directly than to go through some set
> of fully orthogonal combinators purely for the sake of mathematical
> purity.

That is not a problem of purity, that is a problem of simplicity.

> 
> And this goes for Monad, as well. For most of the monads in Haskell,
> the definition of join looks exactly like a definition of (>>= id),
> and it's not very arduous to extend that to (>>= f). But if we do
> define join, then we must recover (>>=) by traversing twice; once for
> map and once for join. There are some examples where join can be
> implemented more efficiently than bind, but I don't actually know of
> any Haskell Monads for which this is the case.
> 
> And as I mentioned earlier, despite many Haskell folks often not
> digging into monads as done by mathematicians much (and that's fine),
> (>>=) does correspond to a nice operation: variable substitution. This
> is true in category theory, when you talk about algebraic theories,
> and it's true in Haskell when you start noticing that various little
> languages are described by algebraic theories. But from this angle, I
> see no reason why it's _better_ to split variable substitution into
> two operations, first turning a tree into a tree of trees, and then
> flattening.

Shouldn't variable substitution be done by mapping?

> 
> It'd be nice if all Functor were a prerequisite for Monad, but even
> then there are still reasons for making (>>=) a primitive.

I do not mean the contrary, and I am very sorry if all readers consider
me as a troll.

> 
> -- Dan