Removing "return" from class Monad

[David Christiansen]

Hello fellow Idris folks,

I've been thinking lately it's somewhat inelegant that all of the
following are true:

1. Every Monad is an Applicative, and Idris' library enfoces this by
having Applicative be a superclass of Monad
2. The "pure" operation on Applicative should always do the same thing
as the "return" operation on Monad
3. Nothing in Idris enforces that "pure" and "return" in fact do the same thing

My proposal to rectify this:

1. Remove "return" from Monad and all instances
2. Define:

return : Monad m => a -> m a
return = pure

This breaks less code.

Pull request 319 [1] implements this change for the standard library.
This would be a breaking change for users, because they will need to
delete "return" from their Monad instances. As this simply reduces
code duplication for any reasonable instance of Monad, it shouldn't be
a big burden.

I figured that because of the compatibility break, it was worth a
mailing list post, and I understand completely if it's rejected.

/David

[1] https://github.com/edwinb/Idris-dev/pull/319