2010-04-23

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

3 comments:

polux said...

Also have a look at "the typeclassopedia" for another natural presentation of the monad laws

Gabriel said...

Your last sentence is misleading. The slides are by Dimino but Lwt is (initially at least) by Vouillon.

Matías Giovannini said...

@Gabriel, thanks for the clarification. I've been sloppy with my due diligence...