From: Jim Pryor Date: Mon, 1 Nov 2010 01:22:40 +0000 (-0400) Subject: week7: update monad intro X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=5406c9244b74b861522ec9c139fcbe08fc30b702 week7: update monad intro Signed-off-by: Jim Pryor --- diff --git a/week7.mdwn b/week7.mdwn index 60f85e5b..da4a4f4b 100644 --- a/week7.mdwn +++ b/week7.mdwn @@ -42,65 +42,133 @@ So what exactly is a monad? As usual, we're not going to be pedantic about it, but for our purposes, we can consider a monad to be a system that provides at least the following three elements: -* A way to build a complex type from some basic type. In the division - example, the polymorphism of the `'a option` type provides a way of - building an option out of any other type of object. People often - use a container metaphor: if `x` has type `int option`, then `x` is - a box that (may) contain an integer. +* A complex type that's built around some more basic type. Usually + it will be polymorphic, and so can apply to different basic types. + In our division example, the polymorphism of the `'a option` type + provides a way of building an option out of any other type of object. + People often use a container metaphor: if `x` has type `int option`, + then `x` is a box that (may) contain an integer. type 'a option = None | Some of 'a;; * A way to turn an ordinary value into a monadic value. In OCaml, we did this for any integer `n` by mapping it to - the option `Some n`. To be official, we can define a function - called unit: + the option `Some n`. In the general case, this operation is + known as `unit` or `return.` Both of those names are terrible. This + operation is only very loosely connected to the `unit` type we were + discussing earlier (whose value is written `()`). It's also only + very loosely connected to the "return" keyword in many other + programming languages like C. But these are the names that the literature + uses. + + The unit/return operation is a way of lifting an ordinary object into + the monadic box you've defined, in the simplest way possible. You can think + of the singleton function as an example: it takes an ordinary object + and returns a set containing that object. In the example we've been + considering: let unit x = Some x;; - val unit : 'a -> 'a option = - So `unit` is a way to put something inside of a box. + So `unit` is a way to put something inside of a monadic box. It's crucial + to the usefulness of monads that there will be monadic boxes that + aren't the result of that operation. In the option/maybe monad, for + instance, there's also the empty box `None`. In another (whimsical) + example, you might have, in addition to boxes merely containing integers, + special boxes that contain integers and also sing a song when they're opened. -* A bind operation (note the type): + The unit/return operation will always be the simplest, conceptually + most straightforward way to lift an ordinary value into a monadic value + of the monadic type in question. - let bind m f = match m with None -> None | Some n -> f n;; +* Thirdly, an operation that's often called `bind`. This is another + unfortunate name: this operation is only very loosely connected to + what linguists usually mean by "binding." In our option/maybe monad, the + bind operation is: + let bind m f = match m with None -> None | Some n -> f n;; val bind : 'a option -> ('a -> 'b option) -> 'b option = - `bind` takes two arguments (a monadic object and a function from - ordinary objects to monadic objects), and returns a monadic - object. + Note the type. `bind` takes two arguments: first, a monadic "box" + (in this case, an 'a option); and second, a function from + ordinary objects to monadic boxes. `bind` then returns a monadic + value: in this case, a 'b option (you can start with, e.g., int options + and end with bool options). Intuitively, the interpretation of what `bind` does is like this: - the first argument computes a monadic object m, which will - evaluate to a box containing some ordinary value, call it `x`. + the first argument is a monadic value m, which + evaluates to a box that (maybe) contains some ordinary value, call it `x`. Then the second argument uses `x` to compute a new monadic value. Conceptually, then, we have - let bind m f = (let x = unwrap m in f x);; + let bind m f = (let x = unbox m in f x);; The guts of the definition of the `bind` operation amount to - specifying how to unwrap the monadic object `m`. In the bind - opertor for the option monad, we unwraped the option monad by - matching the monadic object `m` with `Some n`--whenever `m` - happend to be a box containing an integer `n`, this allowed us to + specifying how to unbox the monadic value `m`. In the bind + opertor for the option monad, we unboxed the option monad by + matching the monadic value `m` with `Some n`---whenever `m` + happened to be a box containing an integer `n`, this allowed us to get our hands on that `n` and feed it to `f`. -So the "option monad" consists of the polymorphic option type, the -unit function, and the bind function. With the option monad, we can + If the monadic box didn't contain any ordinary value, then + we just pass through the empty box unaltered. + + In a more complicated case, like our whimsical "singing box" example + from before, if the monadic value happened to be a singing box + containing an integer `n`, then the `bind` operation would probably + be defined so as to make sure that the result of `f n` was also + a singing box. If `f` also inserted a song, you'd have to decide + whether both songs would be carried through, or only one of them. + + There is no single `bind` function that dictates how this must go. + For each new monadic type, this has to be worked out in an + useful way. + +So the "option/maybe monad" consists of the polymorphic option type, the +unit/return function, and the bind function. With the option monad, we can think of the "safe division" operation 
-# let divide num den = if den = 0 then None else Some (num/den);;
-val divide : int -> int -> int option = 
+# let divide' num den = if den = 0 then None else Some (num/den);;
+val divide' : int -> int -> int option =
as basically a function from two integers to an integer, except with -this little bit of option frill, or option plumbing, on the side. +this little bit of option plumbing on the side. A note on notation: Haskell uses the infix operator `>>=` to stand -for `bind`. I really hate that symbol. Following Wadler, I prefer to -infix five-pointed star, or on a keyboard, `*`. +for `bind`. Chris really hates that symbol. Following Wadler, he prefers to +use an infix five-pointed star, or on a keyboard, `*`. Jim on the other hand +thinks `>>=` is what the literature uses and students won't be able to +avoid it. Moreover, although ⋆ is OK (though not a convention that's been picked up), overloading the multiplication symbol invites its own confusion +and Jim feels very uneasy about that. If not `>>=` then we should use +some other unfamiliar infix symbol (but `>>=` already is such...) + +In any case, the course leaders will work this out somehow. In the meantime, +as you read around, wherever you see `m >>= f`, that means `bind m f`. Also, +if you ever see this notation: + + do + x <- m + f x + +That's a Haskell shorthand for `m >>= (\x -> f x)`, that is, `bind m f`. +Similarly: + + do + x <- m + y <- n + f x y + +is shorthand for `m >>= (\x -> n >>= (\y -> f x y))`, that is, `bind m (fun x +-> bind n (fun y -> f x y))`. Those who did last week's homework may recognize +this. + +(Note that the above "do" notation comes from Haskell. We're mentioning it here +because you're likely to see it when reading about monads. It won't work in +OCaml. In fact, the `<-` symbol already means something different in OCaml, +having to do with mutable record fields. We'll be discussing mutation someday +soon.) The Monad laws