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

On Tue, Oct 16, 2012 at 9:37 PM, AUGER Cédric 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 wrote:

Le Tue, 16 Oct 2012 09:51:29 -0400, Jake McArthur a écrit :

...

On Mon, Oct 15, 2012 at 11:29 PM, Dan Doel 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe