From: jim
Date: Mon, 6 Apr 2015 13:33:28 +0000 (0400)
Subject: refine again
XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=b738e53db95393b5cff000aa84a9b0e4605ac883
refine again

diff git a/topics/week8_reader_monad.mdwn b/topics/week8_reader_monad.mdwn
index 07bba89e..492f7a34 100644
 a/topics/week8_reader_monad.mdwn
+++ b/topics/week8_reader_monad.mdwn
@@ 1,12 +1,10 @@

+
[[!toc levels=2]]
The Reader Monad
================
+[[!toc levels=2]]
The goal for this part is to introduce the Reader Monad, and present
two linguistics applications: binding and intensionality. Along the
+The goal for these notes is to introduce the Reader Monad, and present
+two linguistic applications: binding and intensionality. Along the
way, we'll continue to think through issues related to order, and a
related notion of flow of information.
@@ 54,35 +52,36 @@ ___ ______
No matter what order we evaluate it in, 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
+on the evaluator developed during the previous homework, let's
adopt the following reduction strategy:
> 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 `head'`
+> 2. Reduce `arg` to `arg'`.
+> 3. If `(head' arg')` is a redex, reduce it.
There are many details left unspecified here, but this will be enough
for today. The order in which the computation unfolds will be
> 1. Reduce head (+ 1) to itself
> 2. Reduce arg ((* ((/ 6) 2)) 4)
> 1. Reduce head (* ((/ 6) 2))
> 1. Reduce head * to itself
> 2. Reduce arg ((/ 6) 2)
> 1. Reduce head (/ 6) to itself
> 2. Reduce arg 2 to itself
> 3. Reduce ((/ 6) 2) to 3
> 3. Reduce (* 3) to itself
> 2. Reduce arg 4 to itself
> 3. Reduce ((* 3) 4) to 12
> 3. Reduce ((+ 1) 12) to 13
+> 1. Reduce head `(+ 1)` to itself
+> 2. Reduce arg `((* ((/ 6) 2)) 4)`
+> 1. Reduce head `(* ((/ 6) 2))`
+> 1. Reduce head `*` to itself
+> 2. Reduce arg `((/ 6) 2)`
+> 1. Reduce head `(/ 6)` to itself
+> 2. Reduce arg `2` to itself
+> 3. Reduce `((/ 6) 2)` to `3`
+> 3. Reduce `(* 3)` to itself
+> 2. Reduce arg `4` to itself
+> 3. Reduce `((* 3) 4)` to `12`
+> 3. Reduce `((+ 1) 12)` to `13`
This reduction pattern follows the structure of the original
expression exactly, at each node moving first to the left branch,
processing the left branch, then moving to the right branch, and
finally processing the results of the two subcomputation. (This is
called depthfirst postorder traversal of the tree.)
+called a depthfirst postorder traversal of the tree.)
[diagram with arrows traversing the tree]
@@ 96,7 +95,7 @@ Never mind that these types will allow us to construct silly
arithmetric trees such as `+ *` or `2 3`. Note that during the
reduction sequence, the result of reduction was in every case a
wellformed subtree. So the process of reduction could be animated by
replacing subtrees with the result of reduction on that subtree, till
+replacing subtrees with the result of reduction on that subtree, until
the entire tree is replaced by a single integer (namely, `13`).
Now we replace the number `2` with `0`:
@@ 121,21 +120,21 @@ ___ ______
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
+> 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` at least to `int > int > int option`; but since we now have to
+> 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
@@ 153,15 +152,15 @@ 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:
 â§ (a: 'a) = Some a;;
+ â§ (x : 'a) = Some x
 map2 (g : 'a > 'b > 'c) (xx : 'a option) (yy : 'b option) =
+ 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 (g x y));;
+  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:
@@ 173,7 +172,7 @@ the integers, and by applying `map2` to the operators. Only, we will replace `/`
(match yy with
 None > None
 Some 0 > None
  Some y > Some ((/) x y));;
+  Some y > Some ((/) x y))