index 84a2af5..60f85e5 100644 (file)
@@ -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 = <fun>`
+               val unit : 'a -> 'a option = <fun>

-    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 = <fun>`
+               val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>

-     `bind` takes two arguments (a monadic object and a function from
-     object.
+       `bind` takes two arguments (a monadic object and a function from
+       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

<pre>
# let ( * ) m f = match m with None -> None | Some n -> f n;;
@@ -136,19 +136,19 @@ val unit : 'a -> 'a option = <fun>
- : 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.

-    Some examples of associativity in the option monad:
+       Some examples of associativity in the option monad:

<pre>
# Some 3 * unit * unit;;
@@ -168,7 +168,7 @@ is `*`, pronounced "bind") is an infix operator, so we write
</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
@@ -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,

<pre>
# 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

@@ -225,9 +225,9 @@ intensionality](http://parles.upf.es/glif/pub/sub11/individual/bena_wint.pdf),

All of the code in the discussion below can be found here: [[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.

<pre>
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.