option instead of an int. If we divide 6 by 2, we get the answer Just
3. But if we divide 6 by 0, we get the answer Nothing.
-The next step was to adjust the other arithmetic functions to teach them what to do if they received Nothing instead of a boxed integer.
-This meant
-changing the type of their input from ints to int options. But we
-didn't need to do this piecemeal; rather, we could "lift" the ordinary
-arithmetic operations into the monad using the various tools provided
-by the monad. We'll go over this lifting operation in detail in the next section.
+The next step was to adjust the other arithmetic functions to teach
+them what to do if they received Nothing instead of a boxed integer.
+This meant changing the type of their input from ints to int options.
+But we didn't need to do this piecemeal; rather, we "lift"ed the
+ordinary arithmetic operations into the monad using the various tools
+provided by the monad.
+
+We'll go over this lifting operation in detail in the next section.
## Tracing the effect of safe-div on a larger computation
So let's see how this works in terms of a specific computation.
-<pre>
+<!--
\tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))
+-->
+<pre>
+(+ 1 (* (/ 6 2) 4)) in tree format:
___________
| |
/ 6
</pre>
-This computation should reduce to 13. But given a specific reduction
-strategy, we can watch the order in which the computation proceeds.
-Following on the lambda evaluator developed during the previous
-homework, let's adopt the following reduction strategy:
+No matter which arithmetic operation we begin with, this computation
+should eventually reduce to 13. Given a specific reduction strategy,
+we can watch the order in which the computation proceeds. Following
+on the lambda evaluator developed during the previous homework, let's
+adopt the following reduction strategy:
- In order to reduce (head arg), do the following in order:
+ In order to reduce an expression of the form (head arg), do the following in order:
1. Reduce head to h'
2. Reduce arg to a'.
3. If (h' a') is a redex, reduce it.
finally processing the results of the two subcomputation. (This is
called depth-first postorder traversal of the tree.)
+[diagram with arrows traversing the tree]
+
It will be helpful to see how the types change as we make adjustments.
type num = int
- type contents = Num of num | Op of (num -> num -> num)
+ type contents = Num of num | Op2 of (num -> num -> num)
type tree = Leaf of contents | Branch of tree * tree
Never mind that these types will allow us to construct silly
Now we replace the number 2 with 0:
-<pre>
+<!--
\tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
-
+-->
+<pre>
___________
| |
_|__ ___|___
</pre>
When we reduce, we get quite a ways into the computation before things
-go south:
+break down:
1. Reduce head (+ 1) to itself
2. Reduce arg ((* ((/ 6) 0)) 3)
2. Reduce arg 0 to itself
3. Reduce ((/ 6) 0) to ACKKKK
-This is where we replace `/` with `safe-div`. This means changing the
-type of the arithmetic operators from `int -> int -> int` to
-`int -> int -> int option`; and since we now have to anticipate the
-possibility that any argument might involve division by zero inside of
-it, here is the net result for our types:
+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 Just n, where n is the integer result.
+But if the division attempts to divide by zero, the result is Nothing.
+
+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 here is the net result for our
+types. The easy way to do that is to change (only) the type of num
+from int to int option, leaving everying else the same:
type num = int option
- type contents = Num of num | Op of (num -> num -> num)
+ 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
Then we lift the entire computation into the monad by applying ⇧ to
the integers, and by applying `map2` to the operators:
-<pre>
+<!--
\tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))
-
+-->
+<pre>
___________________
| |
___|____ ____|_____
## Information flowing in the other direction: top to bottom
+We can think of this application as facilitating information flow.
In the save-div example, a subcomputation created a message that
propagated upwards to the larger computation:
form combines with, that is what will be substituted in for free
occurrences of that variable within the body of the lambda.
+## Binding
+
So our next step is to add a (primitive) version of binding to our
-computation. Rather than anticipating any number of binding
-operators, we'll allow for just one binding dependency for now.
+computation. We'll allow for just one binding dependency for now, and
+then generalize later.
-This example is independent of the safe-div example, so we'll return
-to a situation in which the Maybe monad hasn't been added. So the
-types are the ones where numbers are just integers, not int options.
-(In a couple of weeks, we'll start combining monads into a single
-system; if you're impatient, you might think about how to do that now.)
+Binding is independent of the safe division, so we'll return to a
+situation in which the Maybe monad hasn't been added. One of the nice
+properties of programming with monads is that it is possible to add or
+subtract layers according to the needs of the moment. Since we need
+simplicity, we'll set the Maybe monad aside for now.
+
+So we'll go back to the point where the num type is simple int, not
+int options.
type num = int
-And the computation will be without the map2 or the ⇧ from the option
+And we'll start with the computation the map2 or the ⇧ from the option
monad.
As you might guess, the technique we'll use to arrive at binding will
be to use the Reader monad, defined here in terms of m-identity and bind:
- α --> int -> α
+ α ==> int -> α (* The ==> is a Kleisli arrow *)
⇧a = \x.a
u >>= f = \x.f(ux)x
- map2 u v = \x.ux(vx)
+ map f u = \x.f(ux)
+ map2 f u v = \x.f(ux)(vx)
+
A boxed type in this monad will be a function from an integer to an
object in the original type. The unit function ⇧ lifts a value `a` to
When we were dealing with the Maybe monad, a boxed int had type `int
option`. In this monad, a boxed int has type `int -> int`.
-<pre>
+<!--
\tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (x))) (⇧4))))
-
+-->
+<pre>
__________________
| |
___|____ ____|_____
variable will have the type of a boxed int, namely, `int -> int`. So
we have the following:
- x (i:int):int = i
+ x = (\fun (i:int) = i)
That is, variables in this system denote the indentity function!
Take a look at the definition of the reader monad again. The
midentity takes some object `a` and returns `\x.a`. In other words,
-`⇧a = Ka`, so `⇧ = K`. Likewise, `map2` for this monad is the `S`
-combinator. We've seen this before as a strategy for translating a
-lambda abstract into a set of combinators. Here is a part of the
-general scheme for translating a lambda abstract into Combinatory
+`⇧a = Ka`, so `⇧ = K`. Likewise, the reason the `map2` function
+looked familiar is that it is essentially the `S` combinator.
+
+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:
[\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 function is
-that we're making the simplifying assumption that there is at most a
-single lambda involved. So here you see the I (the translation of the
-bound variable), the K and the S.
-
+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 the operation that manages the combination of complex
+expressions.
## Jacobson's Variable Free Semantics as a Reader Monad
-We've designed the discussion so far to make the following claim as
-easy to show as possible: Jacobson's Variable Free Semantics
-(e.g., Jacobson 1999, [Towards a
-Variable-Free
+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/))
-is a reader monad.
+implements a reader monad.
More specifically, it will turn out that Jacobson's geach combinator
*g* is exactly our `lift` operator, and her binding combinator *z* is
-exactly our `bind` (though with the arguments reversed)!
+exactly our `bind` (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
Charlow, with beta reduction as performed by the on-line evaluator:
<pre>
-; Analysis of "Everyone_i thinks he_i left"
-let g = \f g x. f (g x) in
-let z = \f g x. f (g x) x in
+; Jacobson's analysis of "Everyone_i thinks he_i left"
+let g = \f u. \x. f (u x) in
+let z = \f u. \x. f (u x) x in
let he = \x. x in
let everyone = \P. FORALL x (P x) in
~~> FORALL x (thinks (left x) x)
</pre>
-Several things to notice: First, pronouns once again denote identity functions.
-As Jeremy Kuhn has pointed out, this is related to the fact that in
-the mapping from the lambda calculus into combinatory logic that we
-discussed earlier in the course, bound variables translated to I, the
-identity combinator (see additional comments below). We'll return to
-the idea of pronouns as identity functions in later discussions.
+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.
-Third, one of the peculiar aspects of Jacobson's system is that
-binding is accomplished not by applying *z* to the element that will
-(in some pre-theoretic sense) bind the pronoun, here, *everyone*, but
-rather by applying *z* instead to the predicate that will take
-*everyone* as an argument, here, *thinks*.
-
-The basic recipe in Jacobson's system, then, is that you transmit the
+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*. (There are examples with longer chains of *g*'s below.)
-
-Jacobson's *g* combinator is exactly our `lift` operator: it takes a
-functor and lifts it into the monad.
-Furthermore, Jacobson's *z* combinator, which is what she uses to
-create binding links, is essentially identical to our reader-monad
-`bind`!
+with *z*. Here is an example with a longer chain of *g*'s:
<pre>
-everyone (z thinks (g left he))
-
-~~> forall w (thinks (left w) w)
-
everyone (z thinks (g (t bill) (g said (g left he))))
-~~> forall w (thinks (said (left w) bill) w)
+~~> FORALL x (thinks (said (left x) bill) x)
</pre>
-(The `t` combinator is given by `t x = \xy.yx`; it handles situations
-in which English word order places the argument (in this case, a
-grammatical subject) before the predicate.)
+If you compare Jacobson's values for *g* and *z* to the functions in
+the reader monad given above, you'll see that Jacobson's *g*
+combinator is exactly our `map` operator. Furthermore, Jacobson's *z*
+combinator is identital to `>>=`, except with the order of the
+arguments reversed (i.e., `(z f u) == (u >>= f)`).
-So *g* is exactly `lift` (a combination of `bind` and `unit`), and *z*
-is exactly `bind` with the arguments reversed. It appears that
+(The `t` combinator in the derivations above is given by `t x =
+\xy.yx`; it handles situations in which English word order reverses
+the usual function/argument order.)
+
+In other words,
Jacobson's variable-free semantics is essentially a Reader monad.
+One of the peculiar aspects of Jacobson's system is that binding is
+accomplished not by applying *z* to the element that will (in some
+pre-theoretic sense) bind the pronoun, here, *everyone*, but rather by
+applying *z* instead to the predicate that will take *everyone* as an
+argument, here, *thinks*.
+
+
## The Reader monad for intensionality
-Now we'll look at using monads to do intensional function application.
-This is just another application of the Reader monad, not a new monad.
+[This section has not been revised since 2010, so there may be a few
+places where it doesn't follow the convetions we've adopted this time;
+nevertheless, it should be followable.]
+
+Now we'll look at using the Reader monad to do 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