X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week7.mdwn;h=da4a4f4bf22a3b5b732668356dcc4ddd3fec8185;hp=bc8dc8eff4a28cd9cd62865c7becf04ec6ca9e23;hb=5406c9244b74b861522ec9c139fcbe08fc30b702;hpb=7b960aed1552ab5ee4b17428ae4e293decaee2b7;ds=sidebyside diff --git a/week7.mdwn b/week7.mdwn index bc8dc8ef..da4a4f4b 100644 --- a/week7.mdwn +++ b/week7.mdwn @@ -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 = + + 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 = + + 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 = ` - - So `unit` is a way to put something inside of a box. - -* A bind operation (note the type): +
+# let divide' num den = if den = 0 then None else Some (num/den);;
+val divide' : int -> int -> int option = 
+
- `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 = ` +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 ⋆ 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 
 # let ( * ) m f = match m with None -> None | Some n -> f n;;
 val ( * ) : 'a option -> ('a -> 'b option) -> 'b option = 
 # let unit x = Some x;;
 val unit : 'a -> 'a option = 
+
+# 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
-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: 
-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
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, 
 # Some 3 * unit;;
 - : int option = Some 3
+# None * unit;;
+- : 'a option = None
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 , 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. 
 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.