week7: update monad intro
[lambda.git] / week7.mdwn
index bc8dc8e..da4a4f4 100644 (file)
@@ -5,10 +5,10 @@ Monads
 
 Start by (re)reading the discussion of monads in the lecture notes for
 week 6 [Towards Monads](http://lambda.jimpryor.net//week6/#index4h2).
-In those notes, we saw a way to separate thining about error
+In those notes, we saw a way to separate thinking about error
 conditions (such as trying to divide by zero) from thinking about
 normal arithmetic computations.  We did this by making use of the
-Option monad: in each place where we had something of type `int`, we
+option monad: in each place where we had something of type `int`, we
 put instead something of type `int option`, which is a sum type
 consisting either of just an integer, or else some special value which
 we could interpret as signaling that something had gone wrong.
@@ -16,21 +16,21 @@ we could interpret as signaling that something had gone wrong.
 The goal was to make normal computing as convenient as possible: when
 we're adding or multiplying, we don't have to worry about generating
 any new errors, so we do want to think about the difference between
-ints and int options.  We tried to accomplish this by defining a
-`bind` operator, which enabled us to peel away the option husk to get
+`int`s and `int option`s.  We tried to accomplish this by defining a
+`bind` operator, which enabled us to peel away the `option` husk to get
 at the delicious integer inside.  There was also a homework problem
-which made this even more convenient by mapping any bindary operation
+which made this even more convenient by mapping any binary operation
 on plain integers into a lifted operation that understands how to deal
-with int options in a sensible way.
+with `int option`s in a sensible way.
 
 [Linguitics note: Dividing by zero is supposed to feel like a kind of
 presupposition failure.  If we wanted to adapt this approach to
 building a simple account of presupposition projection, we would have
 to do several things.  First, we would have to make use of the
 polymorphism of the `option` type.  In the arithmetic example, we only
-made use of int options, but when we're composing natural language
-expression meanings, we'll need to use types like `N int`, `Det Int`,
-`VP int`, and so on.  But that works automatically, because we can use
+made use of `int option`s, but when we're composing natural language
+expression meanings, we'll need to use types like `N option`, `Det option`,
+`VP option`, and so on.  But that works automatically, because we can use
 any type for the `'a` in `'a option`.  Ultimately, we'd want to have a
 theory of accommodation, and a theory of the situations in which
 material within the sentence can satisfy presuppositions for other
@@ -38,60 +38,137 @@ material that otherwise would trigger a presupposition violation; but,
 not surprisingly, these refinements will require some more
 sophisticated techniques than the super-simple option monad.]
 
-So what examctly is a monad?  As usual, we're not going to be pedantic
+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`.  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 = <fun>
+
+       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. 
+
+       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.
+
+*      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 = <fun>
+
+       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 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 = unbox m in f x);;
+
+       The guts of the definition of the `bind` operation amount 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`.
+
+       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
 
-    `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 an arbitrary integer `n` to
-  the option `Some n`.  To be official, we can define a function
-  called unit:
-
-    `let unit x = Some x;;`
-
-    `val unit : 'a -> 'a option = <fun>`
-
-    So `unit` is a way to put something inside of a box.
-
-* A bind operation (note the type):
+<pre>
+# let divide' num den = if den = 0 then None else Some (num/den);;
+val divide' : int -> int -> int option = <fun>
+</pre>
 
-     `let bind m f = match m with None -> None | Some n -> f n;;`
+as basically a function from two integers to an integer, except with
+this little bit of option plumbing on the side.
 
-     `val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>`
+A note on notation: Haskell uses the infix operator `>>=` to stand
+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 &#8902; 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...)
 
-     `bind` takes two arguments (a monadic object and a function from
-     ordinary objects to monadic objects), and returns a monadic
-     object.
+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:
 
-     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`.
-     Then the second argument uses `x` to compute a new monadic
-     value.  Conceptually, then, we have
+       do
+               x <- m
+               f x
 
-    `let bind m f = (let x = unwrap m in f x);;`
+That's a Haskell shorthand for `m >>= (\x -> f x)`, that is, `bind m f`.
+Similarly:
 
-    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
-    get our hands on that `n` and feed it to `f`.
+       do
+               x <- m
+               y <- n
+               f x y
 
-So the "Option monad" consists of the polymorphic option type, the
-unit function, and the bind function.  
+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.
 
-A note on notation: some people use 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, `*`.
+(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
@@ -100,43 +177,66 @@ The Monad laws
 Just like good robots, monads must obey three laws designed to prevent
 them from hurting the people that use them or themselves.
 
-*    Left identity: unit is a left identity for the bind operation.
-     That is, for all `f:'a -> 'a M`, where `'a M` is a monadic
-     object, we have `(unit x) * f == f x`.  For instance, `unit` is a
-     function of type `'a -> 'a option`, so we have
+*      **Left identity: unit is a left identity for the bind operation.**
+       That is, for all `f:'a -> 'a m`, where `'a m` is a monadic
+       object, we have `(unit x) * f == f x`.  For instance, `unit` is a
+       function of type `'a -> 'a option`, so we have
 
 <pre>
 # let ( * ) m f = match m with None -> None | Some n -> f n;;
 val ( * ) : 'a option -> ('a -> 'b option) -> 'b option = <fun>
 # let unit x = Some x;;
 val unit : 'a -> 'a option = <fun>
+
+# unit 2;;
+- : int option = Some 2
 # unit 2 * unit;;
 - : int option = Some 2
+
+# divide 6 2;;
+- : int option = Some 3
+# unit 2 * divide 6;;
+- : int option = Some 3
+
+# divide 6 0;;
+- : int option = None
+# unit 0 * divide 6;;
+- : int option = None
 </pre>
 
-The parentheses is the magic for telling Ocaml that the
+The parentheses is the magic for telling OCaml that the
 function to be defined (in this case, the name of the function
 is `*`, pronounced "bind") is an infix operator, so we write
 `m * f` or `( * ) m f` instead of `* m f`.
 
-*    Associativity: bind obeys a kind of associativity, like this:
+*      **Associativity: bind obeys a kind of associativity**. Like this:
 
-    `(m * f) * g == m * (fun x -> f x * g)`
+               (m * f) * g == m * (fun x -> f x * g)
 
-    If you don't understand why the lambda form is necessary (the "fun
-    x" part), you need to look again at the type of bind.
+       If you don't understand why the lambda form is necessary (the "fun
+       x" part), you need to look again at the type of bind.
 
-    For an illustration of associativity in the option monad:
+       Some examples of associativity in the option monad:
 
 <pre>
-Some 3 * unit * unit;; 
+Some 3 * unit * unit;; 
 - : int option = Some 3
-Some 3 * (fun x -> unit x * unit);;
+Some 3 * (fun x -> unit x * unit);;
 - : int option = Some 3
+
+# Some 3 * divide 6 * divide 2;;
+- : int option = Some 1
+# Some 3 * (fun x -> divide 6 x * divide 2);;
+- : int option = Some 1
+
+# Some 3 * divide 2 * divide 6;;
+- : int option = None
+# Some 3 * (fun x -> divide 2 x * divide 6);;
+- : int option = None
 </pre>
 
 Of course, associativity must hold for arbitrary functions of
-type `'a -> M 'a`, where `M` is the monad type.  It's easy to
+type `'a -> 'a m`, where `m` is the monad type.  It's easy to
 convince yourself that the bind operation for the option monad
 obeys associativity by dividing the inputs into cases: if `m`
 matches `None`, both computations will result in `None`; if
@@ -145,12 +245,14 @@ computations will again result in `None`; and if the value of
 `f n` matches `Some r`, then both computations will evaluate
 to `g r`.
 
-*    Right identity: unit is a right identity for bind.  That is, 
-     `m * unit == m` for all monad objects `m`.  For instance,
+*      **Right identity: unit is a right identity for bind.**  That is, 
+       `m * unit == m` for all monad objects `m`.  For instance,
 
 <pre>
 # Some 3 * unit;;
 - : int option = Some 3
+# None * unit;;
+- : 'a option = None
 </pre>
 
 Now, if you studied algebra, you'll remember that a *monoid* is an
@@ -162,7 +264,7 @@ serving as the left and right identity.  That is, temporarily using
 presented here, a monad is not exactly a monoid, because (unlike the
 arguments of a monoid operation) the two arguments of the bind are of
 different types.  But if we generalize bind so that both arguments are
-of type `'a -> M 'a`, then we get plain identity laws and
+of type `'a -> 'a m`, then we get plain identity laws and
 associativity laws, and the monad laws are exactly like the monoid
 laws (see <http://www.haskell.org/haskellwiki/Monad_Laws>, near the bottom).
 
@@ -191,9 +293,9 @@ intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),
 though without explicitly using monads.
 
 All of the code in the discussion below can be found here: [[intensionality-monad.ml]].
-To run it, download the file, start Ocaml, and say 
+To run it, download the file, start OCaml, and say 
 
-    # #use "intensionality-monad.ml";;
+       # #use "intensionality-monad.ml";;
 
 Note the extra `#` attached to the directive `use`.
 
@@ -249,15 +351,15 @@ as possible.
 
 So here's what we do:
 
-In Ocaml, we'll use integers to model possible worlds:
+In OCaml, we'll use integers to model possible worlds:
 
-    type s = int;;
-    type e = char;;
-    type t = bool;;
+       type s = int;;
+       type e = char;;
+       type t = bool;;
 
 Characters (characters in the computational sense, i.e., letters like
 `'a'` and `'b'`, not Kaplanian characters) will model individuals, and
-Ocaml booleans will serve for truth values.
+OCaml booleans will serve for truth values.
 
 <pre>
 type 'a intension = s -> 'a;;
@@ -290,7 +392,7 @@ We'll assume that this and the other laws always hold.
 
 We now build up some extensional meanings:
 
-    let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
+       let left w x = match (w,x) with (2,'c') -> false | _ -> true;;
 
 This function says that everyone always left, except for Cam in world
 2 (i.e., `left 2 'c' == false`).
@@ -314,16 +416,16 @@ So Ann left in world 1, but Cam didn't leave in world 2.
 
 A transitive predicate:
 
-    let saw w x y = (w < 2) && (y < x);;
-    extapp (extapp saw bill) ann 1;; (* true *)
-    extapp (extapp saw bill) ann 2;; (* false *)
+       let saw w x y = (w < 2) && (y < x);;
+       extapp (extapp saw bill) ann 1;; (* true *)
+       extapp (extapp saw bill) ann 2;; (* false *)
 
 In world 1, Ann saw Bill and Cam, and Bill saw Cam.  No one saw anyone
 in world two.
 
 Good.  Now for intensions:
 
-    let intapp fn arg w = fn w arg;;
+       let intapp fn arg w = fn w arg;;
 
 The only difference between intensional application and extensional
 application is that we don't feed the evaluation world to the argument.