From: Chris Barker Date: Sun, 31 Oct 2010 14:06:04 +0000 (-0400) Subject: Monads X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=5eb5b091a62e66068007e326cc97ea1faaad2960 Monads --- diff --git a/intensionality-monad.ml b/intensionality-monad.ml new file mode 100644 index 00000000..2f30f8b7 --- /dev/null +++ b/intensionality-monad.ml @@ -0,0 +1,57 @@ +(* This is the intensionality monad discussed in the lecture notes for week 7. *) + +type s = int;; +type e = char;; +type t = bool;; + +type 'a intension = s -> 'a;; +let unit x (w:s) = x;; + +let ann = unit 'a';; +let bill = unit 'b';; +let cam = unit 'c';; + +let bind m f (w:s) = f (m w) w;; +bind (unit 'a') unit 1;; + +let left w x = match (w,x) with (2,'c') -> false | _ -> true;; + +let extapp fn arg w = fn w (arg w);; + +extapp left ann 1;; + +extapp left cam 2;; + +let saw w x y = (w < 2) && (y < x);; +extapp (extapp saw bill) ann 1;; (* true *) +extapp (extapp saw bill) ann 2;; (* false *) + +let intapp fn arg w = fn w arg;; + +let lift pred w arg = bind arg (fun x w -> pred w x) w;; + +intapp (lift left) ann 1;; (* true: Ann still left in world 1 *) +intapp (lift left) cam 2;; (* false: Cam still didn't leave in world 2 *) + +let lift2 pred w arg1 arg2 = + bind arg1 (fun x -> bind arg2 (fun y w -> pred w x y)) w;; +intapp (intapp (lift2 saw) bill) ann 1;; (* true: Ann saw Bill in world 1 *) +intapp (intapp (lift2 saw) bill) ann 2;; (* false: No one saw anyone in world 2 *) + +let think (w:s) (p:s->t) (x:e) = + match (x, p 2) with ('a', false) -> false | _ -> p w;; + +intapp (lift (intapp think + (intapp (lift left) + (unit 'b')))) + (unit 'a') +1;; (* true *) + +intapp (lift (intapp think + (intapp (lift left) + (unit 'c')))) + (unit 'a') +1;; (* false *) + +let swap f x y = f y x;; +bind cam (swap left) 2;; (* false *) diff --git a/week7.mdwn b/week7.mdwn new file mode 100644 index 00000000..812f0496 --- /dev/null +++ b/week7.mdwn @@ -0,0 +1,412 @@ +[[!toc]] + +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 +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 +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. + +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 +at the delicious integer inside. There was also a homework problem +which made this even more convenient by mapping any bindary operation +on plain integers into a lifted operation that understands how to deal +with int options 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 +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 +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 +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. + + 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 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. + + 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);; + + 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. + +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, `*`. + + +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 + +
+# 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 * unit;;
+- : int option = Some 2
+
+ + 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: + + (m * f) * g == m * (fun x -> f x * g) + + If you don't understand why the lambda form is necessary, you need + to look again at the type of bind. This is important. + + For an illustration of associativity in the option monad: + +
+Some 3 * unit * unit;; 
+- : int option = Some 3
+Some 3 * (fun x -> unit x * unit);;
+- : int option = Some 3
+
+ + Of course, associativity must hold for arbitrary functions of + type `'a -> M 'a`, 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 + `m` matches `Some n`, and `f n` evalutes to `None`, then both + 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, + +
+# Some 3 * unit;;
+- : int option = Some 3
+
+ +Now, if you studied algebra, you'll remember that a *monoid* is an +associative operation with a left and right identity. For instance, +the natural numbers along with multiplication form a monoid with 1 +serving as the left and right identity. That is, temporarily using +`*` to mean arithmetic multiplication, `1 * n == n == n * 1` for all +`n`, and `(a * b) * c == a * (b * c)` for all `a`, `b`, and `c`. As +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 +associativity laws, and the monad laws are exactly like the monoid +laws (see ). + + +Monad outlook +------------- + +We're going to be using monads for a number of different things in the +weeks to come. The first main application will be the State monad, +which will enable us to model mutation: variables whose values appear +to change as the computation progresses. Later, we will study the +Continuation monad. + +The intensionality monad +------------------------ + +In the meantime, we'll see a linguistic application for monads: +intensional function application. In Shan (2001) [Monads for natural +language semantics](http://arxiv.org/abs/cs/0205026v1), Ken shows that +making expressions sensitive to the world of evaluation is +conceptually the same thing as making use of a *reader monad* (which +we'll see again soon). This technique was beautifully re-invented +by Ben-Avi and Winter (2007) in their paper [A modular +approach to +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 `# #use +"intensionality-monad.ml"`. + +Here's the idea: since people can have different attitudes towards +different propositions that happen to have the same truth value, we +can't have sentences denoting simple truth values. Then if John +believed that the earth was round, it would force him to believe +Fermat's last theorem holds, since both propositions are equally true. +The traditional solution is to allow sentences to denote a function +from worlds to truth values, what Montague called an intension. +So if `s` is the type of possible worlds, we have the following +situation: + + +
+Extensional types                 Intensional types       Examples
+-------------------------------------------------------------------
+
+S         s->t                    s->t                    John left
+DP        s->e                    s->e                    John
+VP        s->e->t                 s->(s->e)->t            left
+Vt        s->e->e->t              s->(s->e)->(s->e)->t    saw
+Vs        s->t->e->t              s->(s->t)->(s->e)->t    thought
+
+ +This system is modeled on the way Montague arranged his grammar. +(There are significant simplifications: for instance, determiner +phrases are thought of as corresponding to individuals rather than to +generalized quantifiers.) If you're curious about the initial `s`'s +in the extensional types, they're there because the behavior of these +expressions depends on which world they're evaluated at. If you are +in a situation in which you can hold the evaluation world constant, +you can further simplify the extensional types. (Usually, the +dependence of the extension of an expression on the evaluation world +is hidden in a superscript, or built into the lexical interpretation +function.) + +The main difference between the intensional types and the extensional +types is that in the intensional types, the arguments are functions +from worlds to extensions: intransitive verb phrases like "left" now +take intensional concepts as arguments (type s->e) rather than plain +individuals (type e), and attitude verbs like "think" now take +propositions (type s->t) rather than truth values (type t). + +The intenstional types are more complicated than the intensional +types. Wouldn't it be nice to keep the complicated types to just +those attitude verbs that need to worry about intensions, and keep the +rest of the grammar as extensional as possible? This desire is +parallel to our earlier desire to limit the concern about division by +zero to the division function, and let the other functions ignore +division-by-zero problems as much as possible. + +So here's what we do: + +In Ocaml, we'll use integers to model possible worlds: + + 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. + +
+type 'a intension = s -> 'a;;
+let unit x (w:s) = x;;
+
+let ann = unit 'a';;
+let bill = unit 'b';;
+let cam = unit 'c';;
+
+ +In our monad, the intension of an extensional type `'a` is `s -> 'a`, +a function from worlds to extensions. Our unit will be the constant +function (an instance of the K combinator) that returns the same +individual at each world. + +Then `ann = unit 'a'` is a rigid designator: a constant function from +worlds to individuals that returns `'a'` no matter which world is used +as an argument. + +Let's test compliance with the left identity law: + +
+# let bind m f (w:s) = f (m w) w;;
+val bind : (s -> 'a) -> ('a -> s -> 'b) -> s -> 'b = 
+# bind (unit 'a') unit 1;;
+- : char = 'a'
+
+ +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;; + +This function says that everyone always left, except for Cam in world +2 (i.e., `left 2 'c' == false`). + +Then the way to evaluate an extensional sentence is to determine the +extension of the verb phrase, and then apply that extension to the +extension of the subject: + +
+let extapp fn arg w = fn w (arg w);;
+
+extapp left ann 1;;
+# - : bool = true
+
+extapp left cam 2;;
+# - : bool = false
+
+ +`extapp` stands for "extensional function application". +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 *) + +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;; + +The only difference between intensional application and extensional +application is that we don't feed the evaluation world to the argument. +(See Montague's rules of (intensional) functional application, T4 -- T10.) +In other words, instead of taking an extension as an argument, +Montague's predicates take a full-blown intension. + +But for so-called extensional predicates like "left" and "saw", +the extra power is not used. We'd like to define intensional versions +of these predicates that depend only on their extensional essence. +Just as we used bind to define a version of addition that interacted +with the option monad, we now use bind to intensionalize an +extensional verb: + +
+let lift pred w arg = bind arg (fun x w -> pred w x) w;;
+
+intapp (lift left) ann 1;; (* true: Ann still left in world 1 *)
+intapp (lift left) cam 2;; (* false: Cam still didn't leave in world 2 *)
+
+ +Because `bind` unwraps the intensionality of the argument, when the +lifted "left" receives an individual concept (e.g., `unit 'a'`) as +argument, it's the extension of the individual concept (i.e., `'a'`) +that gets fed to the basic extensional version of "left". (For those +of you who know Montague's PTQ, this use of bind captures Montague's +third meaning postulate.) + +Likewise for extensional transitive predicates like "saw": + +
+let lift2 pred w arg1 arg2 = 
+  bind arg1 (fun x -> bind arg2 (fun y w -> pred w x y)) w;;
+intapp (intapp (lift2 saw) bill) ann 1;;  (* true: Ann saw Bill in world 1 *)
+intapp (intapp (lift2 saw) bill) ann 2;;  (* false: No one saw anyone in world 2 *)
+
+ +Crucially, an intensional predicate does not use `bind` to consume its +arguments. Attitude verbs like "thought" are intensional with respect +to their sentential complement, but extensional with respect to their +subject (as Montague noticed, almost all verbs in English are +extensional with respect to their subject; a possible exception is "appear"): + +
+let think (w:s) (p:s->t) (x:e) = 
+  match (x, p 2) with ('a', false) -> false | _ -> p w;;
+
+ +Ann disbelieves any proposition that is false in world 2. Apparently, +she firmly believes we're in world 2. Everyone else believes a +proposition iff that proposition is true in the world of evaluation. + +
+intapp (lift (intapp think
+                     (intapp (lift left)
+                             (unit 'b'))))
+       (unit 'a') 
+1;; (* true *)
+
+ +So in world 1, Ann thinks that Bill left (because in world 2, Bill did leave). + +The `lift` is there because "think Bill left" is extensional wrt its +subject. The important bit is that "think" takes the intension of +"Bill left" as its first argument. + +
+intapp (lift (intapp think
+                     (intapp (lift left)
+                             (unit 'c'))))
+       (unit 'a') 
+1;; (* false *)
+
+ +But even in world 1, Ann doesn't believe that Cam left (even though he +did: `intapp (lift left) cam 1 == true`). Ann's thoughts are hung up +on what is happening in world 2, where Cam doesn't leave. + +*Small project*: add intersective ("red") and non-intersective + adjectives ("good") to the fragment. The intersective adjectives + will be extensional with respect to the nominal they combine with + (using bind), and the non-intersective adjectives will take + intensional arguments. + +Finally, note that within an intensional grammar, extensional funtion +application is essentially just bind: + +
+# let swap f x y = f y x;;
+# bind cam (swap left) 2;;
+- : bool = false
+