Properly Bound

To all practitioners: the type of bind is not the type of >>=. For a monad α m, the latter has type:

val (>>=) : α m → (α → β m) → β m

only because >>= is used as a combinator that allows pipelining computations from left to right, as per usual convention:

… m >>= fun x →
  n >>= fun y →
  …
  return f x y

On the other hand, if you want to take maximum advantage of the Theorems for Free! then your bind should have type:

val bind : (α → β m) → (α m → β m)

because it is a natural transformation, together with return:

val return : α → α m

You can see immediately how both "fit" together; in particular, the second monad law (right identity) falls off naturally (!) from the types:

bind return ≡ id

The first monad law (left identity) is also immediately natural:

bind f ∘ return ≡ f

since bind f's domain coincides with return's range by inspection. The third monad law (associativity) is much less regular but you can see a hint of the mechanics of adjointedness if you read bind g as a whole:

bind g ∘ bind f ≡ bind (bind g ∘ f)

This note is motivated by a reading of Jérémie Dimino's slides about Jérôme Vouillon's Lwt, specifically slide 6 (Edit: thanks Gabriel for the heads up about proper attribution).