week 8 notes

diff --git a/topics/_week8_reader_monad.mdwn b/topics/week8_reader_monad.mdwn
similarity index 80%
rename from topics/_week8_reader_monad.mdwn
rename to topics/week8_reader_monad.mdwn
index af47b3d..4dc0da6 100644 (file)
--- a/topics/_week8_reader_monad.mdwn
+++ b/topics/week8_reader_monad.mdwn
@@ -19,19 +19,24 @@ The starting point was to allow the division function to return an int
 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.  
 
 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.
 
 
 ## 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))))
 \tree ((((+) (1)) (((*) (((/) (6)) (2))) (4))))

+-->
+<pre>
+(+ 1 (* (/ 6 2) 4)) in tree format:

 
  ___________
  |         |
 
  ___________
  |         |


@@ -46,12 +51,13 @@ _|__    ___|___
         /  6
 </pre>
 
         /  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.
     1. Reduce head to h'
     2. Reduce arg to a'.
     3. If (h' a') is a redex, reduce it.


@@ -78,10 +84,12 @@ processing the left branch, then moving to the right branch, and
 finally processing the results of the two subcomputation.  (This is
 called depth-first postorder traversal of the tree.)
 
 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
 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
     type tree = Leaf of contents | Branch of tree * tree
 
 Never mind that these types will allow us to construct silly


@@ -93,9 +101,10 @@ the entire tree is replaced by a single integer (namely, 13).
 
 Now we replace the number 2 with 0:
 
 
 Now we replace the number 2 with 0:
 

-<pre>
+<!--

 \tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))
 \tree ((((+) (1)) (((*) (((/) (6)) (0))) (4))))

-
+-->
+<pre>

  ___________
  |         |
 _|__    ___|___
  ___________
  |         |
 _|__    ___|___


@@ -110,7 +119,7 @@ _|__    ___|___
 </pre>
 
 When we reduce, we get quite a ways into the computation before things
 </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)
 
     1. Reduce head (+ 1) to itself
     2. Reduce arg ((* ((/ 6) 0)) 3)


@@ -121,14 +130,21 @@ go south:
                    2. Reduce arg 0 to itself
                    3. Reduce ((/ 6) 0) to ACKKKK
 
                    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 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
     type tree = Leaf of contents | Branch of tree * tree
 
 The only difference is that instead of defining our numbers to be


@@ -151,9 +167,10 @@ is the ⇧ and the map2 function from the notes on safe division:
 Then we lift the entire computation into the monad by applying ⇧ to
 the integers, and by applying `map2` to the operators:
 
 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))))
 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (⇧0))) (⇧4))))

-
+-->
+<pre>

      ___________________
      |                 |
   ___|____         ____|_____
      ___________________
      |                 |
   ___|____         ____|_____


@@ -208,6 +225,7 @@ till it comes out of the result faucet at the top of the tree.
 
 ## Information flowing in the other direction: top to bottom
 
 
 ## 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:
 
 In the save-div example, a subcomputation created a message that
 propagated upwards to the larger computation:
 


@@ -252,28 +270,35 @@ embedded position.  Whatever the value of the argument that the lambda
 form combines with, that is what will be substituted in for free
 occurrences of that variable within the body of the lambda.
 
 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
 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
 
 
     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:
 
 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
     ⇧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
 
 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


@@ -301,9 +326,10 @@ That is, `num` is once again replaced with the type of a boxed int.
 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`.
 
 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))))
 \tree ((((map2 +) (⇧1)) (((map2 *) (((map2 /) (⇧6)) (x))) (⇧4))))

-
+-->
+<pre>

      __________________
      |                |
   ___|____        ____|_____
      __________________
      |                |
   ___|____        ____|_____


@@ -324,7 +350,7 @@ 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:
 
 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!
 
 
 That is, variables in this system denote the indentity function!
 


@@ -333,10 +359,12 @@ from any integer `x` to `(+ 1 (* (/ 6 x)) 4)`.
 
 Take a look at the definition of the reader monad again.  The
 midentity takes some object `a` and returns `\x.a`.  In other words,
 
 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:
 
 Logic.  The translation function `[.]` translates a lambda term into a
 term in Combinatory Logic:
 


@@ -345,24 +373,25 @@ term in Combinatory Logic:
     [\a.M] = K[M]       (assuming a not free in M)
     [\a.(MN)] = S[\a.M][\a.N]
 
     [\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
 
 
 ## 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/))
 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
 
 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
 
 Jacobson's system contains two main combinators, *g* and *z*.  She
 calls *g* the Geach rule, and *z* performs binding.  Here is a typical


@@ -370,9 +399,9 @@ computation.  This implementation is based closely on email from Simon
 Charlow, with beta reduction as performed by the on-line evaluator:
 
 <pre>
 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
 
 let he = \x. x in
 let everyone = \P. FORALL x (P x) in
 


@@ -381,55 +410,51 @@ everyone (z thinks (g left he))
 ~~>  FORALL x (thinks (left x) x)
 </pre>
 
 ~~>  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.
 
 
 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
 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>
 
 <pre>

-everyone (z thinks (g left he))
-
-~~> forall w (thinks (left w) w)
-

 everyone (z thinks (g (t bill) (g said (g left he))))
 
 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>
 
 </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.
 
 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
 
 ## 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
 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