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

[AUGER Cédric]

Le Wed, 24 Oct 2012 12:36:52 +0700,
Kim-Ee Yeoh <ky3 at atamo.com> a écrit :

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

It is not my wish to be a troller. So please keep or don't keep your
point of view on that matter, and I'll keep mine.

bind is an injection of a Kleisli category to the Hask category to
allow composition,
return is the identity of that same Kleisli category.

I do not pretend <return,bind> to be useless, just that the name
"Monad" does not fit very well. I do not want to fight the people who
have chosen this name, which has spread to many other paradigms. I just
say that it is not very fortunate.

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

Once again that set is not uninteresting, just the name does not fit
very well. And for your comment on proofs, I am perfectly aware of the
Curry Howard correspondance, and that proofs given by Haskell programs
are not very interesting from a mathematical point of view (beside the
fact that this system is unsound, ie. any statement [ie. a type] can
be proved [ie. admits a program of that type], due to the "undefined"
value [I do not want to enter a new troll of wether "undefined" is or
is not a value, if the word value does not please you, replace it]).

> I don't understand your dogmatism about return and join being
> canonically the best monad definition in all possible mathematics.

I am not that dogmatic, if I need to write a program on Haskell, I
won't cry because I will produce some "IO stuff".

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