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

Le Wed, 24 Oct 2012 12:36:52 +0700, Kim-Ee Yeoh a écrit :

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.

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