Now we'll look at using monads to do intensional function application.
-This really is just another application of the reader monad, not a new monad.
+This really is just another application of the Reader monad, not a new monad.
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 the reader monad.
+the same thing as making use of the Reader monad.
This technique was beautifully re-invented
by Ben-Avi and Winter (2007) in their paper [A modular
approach to
let left1 (x:e) = true;;
let saw1 (x:e) (y:e) = y < x;;
- left1 ann;;
+ left1 ann;; (* true *)
saw1 bill ann;; (* true *)
saw1 ann bill;; (* false *)
So here's our extensional system: everyone left, including Ann;
-and Ann saw Bill, but Bill didn't see Ann. (Note that Ocaml word
-order is VOS, verb-object-subject.)
+and Ann saw Bill (`saw1 bill ann`), but Bill didn't see Ann. (Note that the word
+order we're using is VOS, verb-object-subject.)
Now we add intensions. Because different people leave in different
worlds, the meaning of *leave* must depend on the world in which it is
<pre>
type 'a intension = s -> 'a;;
let unit x = fun (w:s) -> x;;
-let bind m f = fun (w:s) -> f (m w) w;;
+let bind u f = fun (w:s) -> f (u w) w;;
</pre>
Then the individual concept `unit ann` is a rigid designator: a
matter which world is used as an argument. This is a typical kind of
thing for a monad unit to do.
-Then combining a prediction like *left* which is extensional in its
+Then combining a predicate like *left* which is extensional in its
subject argument with an intensional subject like `unit ann` is simply bind
in action:
We can arrange for an extensional transitive verb to take intensional
arguments:
- let lift f u v = bind u (fun x -> bind v (fun y -> f x y));;
+ let lift2 f u v = bind u (fun x -> bind v (fun y -> f x y));;
This is the exact same lift predicate we defined in order to allow
addition in our division monad example.
<pre>
-lift saw (unit bill) (unit ann) 1;; (* true *)
-lift saw (unit bill) (unit ann) 2;; (* false *)
+lift2 saw (unit bill) (unit ann) 1;; (* true *)
+lift2 saw (unit bill) (unit ann) 2;; (* false *)
</pre>
Ann did see bill in world 1, but Ann didn't see Bill in world 2.
bind (unit ann) (thinks (bind (unit cam) left)) 1;;
-But even in world 1, Ann doesn't believe that Cam left (even though he
-did: `bind (unit cam) left 1 == true`). Ann's thoughts are hung up on
+But in world 1, Ann doesn't believe that Cam left (even though he
+did leave in world 1: `bind (unit cam) left 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