```(+ 1 (* (/ 6 2) 4)) in tree format:

___________
|         |
_|__    ___|___
|  |    |     |
+  1  __|___  4
|    |
*  __|___
|    |
_|__  2
|  |
/  6
```
``` ___________
|         |
_|__    ___|___
|  |    |     |
+  1  __|___  4
|    |
*  __|___
|    |
_|__  0
|  |
/  6
```
When we reduce, we get quite a ways into the computation before things break down: > 1. Reduce head `(+ 1)` to itself > 2. Reduce arg `((* ((/ 6) 0)) 4)` > 1. Reduce head `(* ((/ 6) 0))` > 1. Reduce head `*` to itself > 2. Reduce arg `((/ 6) 0)` > 1. Reduce head `(/ 6)` to itself > 2. Reduce arg `0` to itself > 3. Reduce `((/ 6) 0)` to ACKKKK This is where we replace `/` with `safe_div`. `safe_div` returns not an `int`, but an `int option`. If the division goes through, the result is `Some n`, where `n` is the integer result. But if the division attempts to divide by zero, the result is `None`. We could try changing the type of the arithmetic operators from `int -> int -> int` to `int -> int -> int option`; but since we now have to anticipate the possibility that *any* argument might involve division by zero inside of it, it would be better to prepare for the possibility that any subcomputation might return `None` here. So our operators should have the type `int option -> int option -> int option`. Let's bring that about by just changing the type `num` from `int` to `int option`, leaving everying else the same: type num = int option type contents = Num of num | Op2 of (num -> num -> num) type tree = Leaf of contents | Branch of tree * tree The only difference is that instead of defining our numbers to be simple integers, they are now `int option`s; and so `Op` is an operator over `int option`s. At this point, we bring in the monadic machinery. In particular, here is the `⇧` and the `map2` function from the notes on safe division: ⇧ (x : 'a) = Some x map2 (f : 'a -> 'b -> 'c) (xx : 'a option) (yy : 'b option) = match xx with | None -> None | Some x -> (match yy with | None -> None | Some y -> Some (f x y)) Then we lift the entire computation into the monad by applying `⇧` to the integers, and by applying `map2` to the operators. Only, we will replace `/` with `safe_div`, defined as follows: safe_div (xx : 'a option) (yy : 'b option) = match xx with | None -> None | Some x -> (match yy with | None -> None | Some 0 -> None | Some y -> Some ((/) x y))
```     ___________________
|                 |
___|____         ____|_____
|      |         |        |
map2 +  ⇧1    _____|_____  ⇧4
|         |
map2 *  ____|____
|       |
___|____  ⇧0
|      |
safe_div  ⇧6
```
With these adjustments, the faulty computation now completes smoothly: > 1. Reduce head `((map2 +) ⇧1)` > 2. Reduce arg `(((map2 *) ((safe_div ⇧6) ⇧0)) ⇧4)` > 1. Reduce head `((map2 *) ((safe_div ⇧6) ⇧0))` > 1. Reduce head `(map2 *)` > 2. Reduce arg `((safe_div ⇧6) ⇧0)` > 1. Reduce head `(safe_div ⇧6)` > 2. Reduce arg `⇧0` > 3. Reduce `((safe_div ⇧6) ⇧0)` to `None` > 3. Reduce `((map2 *) None)` > 2. Reduce arg `⇧4` > 3. Reduce `(((map2 *) None) ⇧4)` to `None` > 3. Reduce `(((map2 +) ⇧1) None)` to `None` As soon as we try to divide by `0`, `safe_div` returns `None`. Thanks to the details of `map2`, the fact that `None` has been returned by one of the arguments of a `map2`-ed operator guarantees that the `map2`-ed operator will pass on the `None` as its result. So the result of each enclosing computation will be `None`, up to the root of the tree. It is unfortunate that we need to continue the computation after encountering our first `None`. We know immediately at the result of the entire computation will be `None`, yet we continue to compute subresults and combinations. It would be more efficient to simply jump to the top as soon as `None` is encoutered. Let's call that strategy Abort. We'll arrive at an `Abort` operator later in the semester. So at this point, we can see how the Option/Maybe monad provides plumbing that allows subcomputations to send information from one part of the computation to another. In this case, the `safe_div` function can send the information that division by zero has been attempted upwards to the rest of the computation. If you think of the plumbing as threaded through the tree in depth-first, postorder traversal, then `safe_div` drops `None` into the plumbing half way through the computation, and that `None` travels through the rest of the plumbing till it comes out of the result faucet at the top of the tree. ## Information flowing in the other direction: top to bottom We can think of this application as facilitating information flow. In the `safe_div` example, a subcomputation created a message that propagated upwards to the larger computation:
```                 message: Division by zero occurred!
^
___________          |
|         |          |
_|__    ___|___       |
|  |    |     |       |
+  1  __|___  4       |
|    |          |
*  __|___  -----|
|    |
_|__  0
|  |
/  6
```
(The message was implemented by `None`.) We might want to reverse the direction of information flow, making information available at the top of the computation available to the subcomputations:
```                    [λn]
___________          |
|         |          |
_|__    ___|___       |
|  |    |     |       |
+  1  __|___  4       |
|    |          |
*  __|___       |
|    |       |
_|__  n  <----|
|  |
/  6
```
```type α = int -> α
⇧x = \n. x
xx >>= k = \n. k (xx n) n
map  f xx = \n. f (xx n)
ff ¢ xx = \n. (ff n) (xx n)
map2 f xx yy = map f xx ¢ yy = \n. f (xx n) (yy n)
```
```     __________________
|                |
___|____        ____|_____
|      |        |        |
map2 +  ⇧1    ____|_____  ⇧4
|        |
map2 *  ___|____
|      |
___|____  x
|      |
map2 /  ⇧6
```
It remains only to decide how the variable `n` will access the input value supplied at the top of the tree. The input value is supposed to be the value that gets used for the variable `n`. Like every leaf in the tree in argument position, the code we want in order to represent the variable will have the type of a boxed `int`, namely, `int -> int`. So we have the following: var_n = fun (n : int) -> n That is, variables in this system denote the identity function! The result of evaluating this tree will be a boxed integer: a function from any integer `n` to `(+ 1 (* (/ 6 n)) 4)`. Take a look at the definition of the Reader monad again. The `mid` takes some object `x` and returns `\n. x`. In other words, `⇧x = Kx`, for our familiar combinator **K**, so `⇧ = K`. Likewise, the `map` operation is just function composition, and the `mapply`/`¢` operation is our friend the **S** combinator. `map2 f xx yy` for the Reader monad is `(f ○ xx) ¢ yy` or `S (f ○ xx) yy`. We've seen this before as a strategy for translating a binding construct into a set of combinators. To remind you, here is a part of the general scheme for translating a lambda abstract into Combinatory Logic. The translation function `[.]` translates a lambda term into a term in Combinatory Logic: [(MN)] = ([M] [N]) [\a.a] = I [\a.M] = K[M] (assuming a not free in M) [\a.(MN)] = S[\a.M][\a.N] The reason we can make do with this subset of the full translation scheme is that we're making the simplifying assumption that there is at most a single lambda involved. So once again we have the identity function **I** as the translation of the bound variable, **K** as the function governing expressions that don't contain an instance of the bound variable, **S** as an operation that manages `¢`, that is, the applicative combination of complex expressions. ## Jacobson's Variable Free Semantics as a Reader Monad We've designed the presentation above to make it as easy as possible to show that Jacobson's Variable Free Semantics (e.g., Jacobson 1999, [Towards a Variable-Free Semantics](http://www.springerlink.com/content/j706674r4w217jj5/)) implements a Reader monad. More specifically, it will turn out that Jacobson's geach combinator *g* is exactly our `map` operator, and her binding combinator *z* is exactly our `mbind` (though with the arguments reversed). Jacobson's system contains two main combinators, *g* and *z*. She calls *g* the Geach rule, and *z* performs binding. Here is a typical computation. This implementation is based closely on email from Simon Charlow, with beta reduction as performed by the on-line evaluator:
```; Jacobson's analysis of "Everyone_i thinks he_i left"
let g = \f xx. \n. f (xx n) in ; or `f ○ xx`
let z = \k xx. \n. k (xx n) n in ; or `S (flip k) xx`, or `Reader.(>>=) xx k`
let he = \n. n in
let everyone = \P. FORALL i (P i) in

everyone (z thinks (g left he))

~~>  FORALL i (thinks (left i) i)
```
Two things to notice: First, pronouns once again denote identity functions, just as we saw in the reader monad in the previous section. Second, *g* plays the role of transmitting a binding dependency for an embedded constituent to a containing constituent. The basic recipe in Jacobson's system is that you transmit the dependence of a pronoun upwards through the tree using *g* until just before you are about to combine with the binder, when you finish off with *z*. Here is an example with a longer chain of *g*'s:
```; "Everyone_i thinks that Bill said he_i left"

everyone (z thinks (g (T bill) (g said (g left he))))
; or `everyone (thinks =<< T bill ○ said ○ left ○ I)`

~~> FORALL i (thinks (said (left i) bill) i)
```
```Extensional types              Intensional types       Examples
-------------------------------------------------------------------

S         t                    s->t                    John left
DP        e                    s->e                    John
VP        e->t                 (s->e)->s->t            left
Vt        e->e->t              (s->e)->(s->e)->s->t    saw
Vs        t->e->t              (s->t)->(s->e)->s->t    thought
```
This system is modeled on the way Montague arranged his grammar. There are significant simplifications compared to Montague: for instance, determiner phrases are thought of here as corresponding to individuals rather than to generalized quantifiers. 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 so-called "individual 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`). In addition, the result of each predicate is an intension. This expresses the fact that the set of people who left in one world may be different than the set of people who left in a different world. Normally, the dependence of the extension of a predicate to the world of evaluation is hidden inside of an evaluation coordinate, or built into the the lexical meaning function, but we've made it explicit here in the way that the intensionality monad makes most natural. The intensional types are more complicated than the extensional types. Wouldn't it be nice to make the complicated types available for expressions like 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, like addition or multiplication, 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. `char`s (characters in the computational sense, i.e., letters like `'a'` and `'b'`, not Kaplanian characters) will model individuals, and OCaml `bool`s will serve for truth values: type s = int type e = char type t = bool let ann = 'a' let bill = 'b' let cam = 'c' let left1 (x : e) = true let saw1 (y : e) (x : e) = x < y 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 (`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 being evaluated: let left (x : e) (w : s) = match (x, w) with ('c', 2) -> false | _ -> true left ann 1 (* true: Ann left in world 1 *) left cam 2 (* false: Cam didn't leave in world 2 *) This new definition says that everyone always left, except that in world 2, Cam didn't leave. Note that although this general *left* is sensitive to world of evaluation, it does not have the fully intensionalized type given in the chart above, which was `(s->e)->s->t`. This is because *left* does not exploit the additional resolving power provided by making the subject an individual concept. In semantics jargon, we say that *leave* is extensional with respect to its first argument. We will adopt the general strategy of defining predicates in a way that they take arguments of the lowest type that will allow us to make all the distinctions the predicate requires. When it comes time to combine this predicate with monadic arguments, we'll have to make use of various lifting predicates. Likewise, although *see* depends on the world of evaluation, it is extensional in both of its syntactic arguments: let saw (y : e) (x : e) (w : s) = (w < 2) && (x < y) saw bill ann 1 (* true: Ann saw Bill in world 1 *) saw bill ann 2 (* false: no one saw anyone in world 2 *) This (again, partially) intensionalized version of *see* coincides with the `saw1` function we defined above for world 1; in world 2, no one saw anyone. Just to keep things straight, let's review the facts:
```     World 1: Everyone left.
Ann saw Bill, Ann saw Cam, Bill saw Cam, no one else saw anyone.
World 2: Ann left, Bill left, Cam didn't leave.
No one saw anyone.
```
```type 'a intension = s -> 'a
```let map2' f xx yy = xx >>= (fun x -> yy >>= (fun y -> f x y))
This is almost the same `map2` predicate we defined in order to allow addition in our division monad example. The *difference* is that this variant operates on verb meanings that take extensional arguments but returns an intensional result. Thus the original `map2` predicate has `mid (f x y)` where we have just `f x y` here. The use of `>>=` here to combine *left* with an individual concept, and the use of `map2'` to combine *see* with two intensional arguments closely parallels the two of Montague's meaning postulates (in PTQ) that express the relationship between extensional verbs and their uses in intensional contexts.
```map2' saw (mid bill) (mid ann) 1  (* true *)