On Tue, Oct 16, 2012 at 9:37 PM, AUGER Cédric <span dir="ltr"><<a href="mailto:sedrikov@gmail.com" target="_blank">sedrikov@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
As I said, from the mathematical point of view, join (often noted μ in<br>category theory) is the (natural) transformation which with return (η<br>that I may have erroneously written ε in some previous mail) defines a<br>
monad (and requires some additionnal law). </blockquote><div><br></div><div>Auger:</div><div><br></div><div>Your emails keep invoking "the mathematical point of view" as if it were something unique and universal.</div>
<div><br></div><div>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.</div>
<div><br></div><div>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.</div><div><br>
</div>-- Kim-Ee<br>
<br><br><div class="gmail_quote">On Tue, Oct 16, 2012 at 9:37 PM, AUGER Cédric <span dir="ltr"><<a href="mailto:sedrikov@gmail.com" target="_blank">sedrikov@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Le Tue, 16 Oct 2012 09:51:29 -0400,<br>
Jake McArthur <<a href="mailto:jake.mcarthur@gmail.com">jake.mcarthur@gmail.com</a>> a écrit :<br>
<div class="im"><br>
> On Mon, Oct 15, 2012 at 11:29 PM, Dan Doel <<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>> wrote:<br>
</div><div class="im">> > I'd be down with putting join in the class, but that tends to not be<br>
> > terribly important for most cases, either.<br>
><br>
> Join is not the most important, but I do think it's often easier to<br>
> define than bind. I often find myself implementing bind by explicitly<br>
> using join.<br>
<br>
</div>join IS the most important from the categorical point of view.<br>
In a way it is natural to define 'bind' from 'join', but in Haskell, it<br>
is not always possible (see the Monad/Functor problem).<br>
<br>
As I said, from the mathematical point of view, join (often noted μ in<br>
category theory) is the (natural) transformation which with return (η<br>
that I may have erroneously written ε in some previous mail) defines a<br>
monad (and requires some additionnal law). As often some points it out,<br>
Haskellers are not very right in their definition of Monad, not because<br>
of the bind vs join (in fact in a Monad either of them can be defined<br>
from the other one), but because of the functor status of a Monad. A<br>
monad, should always be a functor (at least to fit its mathematical<br>
definition). And this problem with the functor has probably lead to the<br>
use of "bind" (which is polymorphic in two type variables) rather than<br>
"join" (which has only one type variable, and thus is simpler).<br>
The problem, is that when 'm' is a Haskell Monad which does not belong<br>
to the Functor class, we cannot define 'bind' in general from 'join'.<br>
<br>
That is in the context where you have:<br>
<br>
return:∀ a. a → (m a)<br>
join:∀ a. (m (m a)) → (m a)<br>
x:m a<br>
f:a → (m b)<br>
<br>
you cannot define some term of type 'm b', since you would need to use<br>
at the end, either 'f' (and you would require to produce a 'a' which<br>
would be impossible), or 'return' (and you would need to produce a 'b',<br>
which is impossible), or 'join' (and you would need to produce a 'm (m<br>
b)', and recursively for that you cannot use return which would make<br>
you go back to define a 'm b' term)<br>
<br>
For that, you need the 'fmap' operation of the functor.<br>
<br>
return:∀ a. a → (m a)<br>
join:∀ a. (m (m a)) → (m a)<br>
fmap:∀ a b. (a→b) → ((m a)→(m b))<br>
x:m a<br>
f:a → (m b)<br>
<br>
in this context defining a term of type 'm b' is feasible (join (fmap f<br>
x)), so that you can express "bind = \ x f -> join (fmap f x)".<br>
<br>
To sum up, mathematical monads are defined from 'return' and 'join' as<br>
a mathematical monad is always a functor (so 'fmap' is defined, and<br>
'bind', which is more complex than 'join' can be defined from 'join'<br>
and 'fmap'). Haskell does not use a very good definition for their<br>
monads, as they may not be instance of the Functor class (although<br>
most of them can easily be defined as such), and without this 'fmap',<br>
'join' and 'return' would be pretty useless, as you wouldn't be able<br>
to move from a type 'm a' to a type 'm b'.<br>
<div class="HOEnZb"><div class="h5"><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>