From: Jim Pryor Date: Mon, 1 Nov 2010 00:42:29 +0000 (-0400) Subject: week7: housecleaning X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=726437adf263c434a88cfe7d56e4b04b060d70b4;hp=a514805caa6f1ca2ac4bad1674fbc74622e71968 week7: housecleaning Signed-off-by: Jim Pryor --- diff --git a/week7.mdwn b/week7.mdwn index 84a2af55..60f85e5b 100644 --- a/week7.mdwn +++ b/week7.mdwn @@ -29,8 +29,8 @@ 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 option`s, 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 +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 @@ -42,49 +42,49 @@ 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 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. - `type 'a option = None | Some of 'a;;` + 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: +* 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: - `let unit x = Some x;;` + let unit x = Some x;; - `val unit : 'a -> 'a option = ` + 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 box. -* A bind operation (note the type): +* A bind operation (note the type): - `let bind m f = match m with None -> None | Some n -> f n;;` + let bind m f = match m with None -> None | Some n -> f n;; - `val bind : 'a option -> ('a -> 'b option) -> 'b option = ` + 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. + `bind` takes two arguments (a monadic object and a function from + ordinary objects to monadic objects), and returns a monadic + object. - 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 + 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 - `let bind m f = (let x = unwrap m in f x);;` + let bind m f = (let x = unwrap 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 - get our hands on that `n` and feed it to `f`. + 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`. So the "option monad" consists of the polymorphic option type, the unit function, and the bind function. With the option monad, we can @@ -109,10 +109,10 @@ 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;;
@@ -136,19 +136,19 @@ val unit : 'a -> 'a option = 
 - : 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. - Some examples of associativity in the option monad: + Some examples of associativity in the option monad: 
 # Some 3 * unit * unit;; 
@@ -168,7 +168,7 @@ is `*`, pronounced "bind") is an infix operator, so we write
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 @@ -177,8 +177,8 @@ 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;;
@@ -196,7 +196,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).
 
@@ -225,9 +225,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`.
 
@@ -283,15 +283,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;;
@@ -324,7 +324,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`).
@@ -348,16 +348,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.