On Tue, Oct 16, 2012 at 9:37 PM, AUGER Cédric <span dir="ltr">&lt;<a href="mailto:sedrikov@gmail.com" target="_blank">sedrikov@gmail.com</a>&gt;</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 &quot;the mathematical point of view&quot; 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&#39;t understand your dogmatism about return and join being canonically the best monad definition in all possible mathematics. That&#39;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">&lt;<a href="mailto:sedrikov@gmail.com" target="_blank">sedrikov@gmail.com</a>&gt;</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 &lt;<a href="mailto:jake.mcarthur@gmail.com">jake.mcarthur@gmail.com</a>&gt; a écrit :<br>
<div class="im"><br>
&gt; On Mon, Oct 15, 2012 at 11:29 PM, Dan Doel &lt;<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>&gt; wrote:<br>
</div><div class="im">&gt; &gt; I&#39;d be down with putting join in the class, but that tends to not be<br>
&gt; &gt; terribly important for most cases, either.<br>
&gt;<br>
&gt; Join is not the most important, but I do think it&#39;s often easier to<br>
&gt; define than bind. I often find myself implementing bind by explicitly<br>
&gt; 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 &#39;bind&#39; from &#39;join&#39;, 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 &quot;bind&quot; (which is polymorphic in two type variables) rather than<br>
&quot;join&quot; (which has only one type variable, and thus is simpler).<br>
The problem, is that when &#39;m&#39; is a Haskell Monad which does not belong<br>
to the Functor class, we cannot define &#39;bind&#39; in general from &#39;join&#39;.<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 &#39;m b&#39;, since you would need to use<br>
at the end, either &#39;f&#39; (and you would require to produce a &#39;a&#39; which<br>
would be impossible), or &#39;return&#39; (and you would need to produce a &#39;b&#39;,<br>
which is impossible), or &#39;join&#39; (and you would need to produce a &#39;m (m<br>
b)&#39;, and recursively for that you cannot use return which would make<br>
you go back to define a &#39;m b&#39; term)<br>
<br>
For that, you need the &#39;fmap&#39; 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 &#39;m b&#39; is feasible (join (fmap f<br>
x)), so that you can express &quot;bind = \ x f -&gt; join (fmap f x)&quot;.<br>
<br>
To sum up, mathematical monads are defined from &#39;return&#39; and &#39;join&#39; as<br>
a mathematical monad is always a functor (so &#39;fmap&#39; is defined, and<br>
&#39;bind&#39;, which is more complex than &#39;join&#39; can be defined from &#39;join&#39;<br>
and &#39;fmap&#39;). 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 &#39;fmap&#39;,<br>
&#39;join&#39; and &#39;return&#39; would be pretty useless, as you wouldn&#39;t be able<br>
to move from a type &#39;m a&#39; to a type &#39;m b&#39;.<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>