X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=zipper-lists-continuations.mdwn;h=326d0e54981fbb93052d08112ae50a99e7fe5cba;hp=8c052f0e22c42b5470d1c723c4753dc875b6df2a;hb=ed41d27c213c6eed4432fb353974fa9b8e30c75a;hpb=ba3453bf9e8df1a8bc0abf42727cc1a3fcda9540

diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
index 8c052f0e..326d0e54 100644
--- a/zipper-lists-continuations.mdwn
+++ b/zipper-lists-continuations.mdwn
@@ -5,9 +5,7 @@ continuation monad.
 
 The three approches are:
 
-*    Rethinking the list monad;
-*    Montague's PTQ treatment of DPs as generalized quantifiers; and
-*    Refunctionalizing zippers (Shan: zippers are defunctionalized continuations);
+[[!toc]]
 
 Rethinking the list monad
 -------------------------
@@ -28,10 +26,10 @@ constructor is
 
 then we can deduce the unit and the bind:
 
-    runit x:'a -> 'a reader = fun (e:env) -> x
+    r_unit x:'a -> 'a reader = fun (e:env) -> x
 
 Since the type of an `'a reader` is `fun e:env -> 'a` (by definition),
-the type of the `runit` function is `'a -> e:env -> 'a`, which is a
+the type of the `r_unit` function is `'a -> e:env -> 'a`, which is a
 specific case of the type of the *K* combinator.  So it makes sense
 that *K* is the unit for the reader monad.
 
@@ -45,24 +43,30 @@ We can deduce the correct `bind` function as follows:
 
 We have to open up the `u` box and get out the `'a` object in order to
 feed it to `f`.  Since `u` is a function from environments to
-objects of type `'a`, we'll have
+objects of type `'a`, the way we open a box in this monad is
+by applying it to an environment:
 
          .... f (u e) ...
 
 This subexpression types to `'b reader`, which is good.  The only
-problem is that we don't have an `e`, so we have to abstract over that
-variable:
+problem is that we invented an environment `e` that we didn't already have ,
+so we have to abstract over that variable to balance the books:
 
          fun e -> f (u e) ...
 
 This types to `env -> 'b reader`, but we want to end up with `env ->
-'b`.  The easiest way to turn a 'b reader into a 'b is to apply it to
+'b`.  Once again, the easiest way to turn a `'b reader` into a `'b` is to apply it to
 an environment.  So we end up as follows:
 
     r_bind (u:'a reader) (f:'a -> 'b reader):('b reader) = f (u e) e         
 
 And we're done.
 
+[This bind is a simplified version of the careful `let a = u e in ...`
+constructions we provided in earlier lectures.  We use the simplified
+versions here in order to emphasize similarities of structure across
+monads; the official bind is still the one with the plethora of `let`'s.]
+
 The **State Monad** is similar.  We somehow intuit that we want to use
 the following type constructor:
 
@@ -117,7 +121,7 @@ And sure enough,
 But where is the reasoning that led us to this unit and bind?
 And what is the type `['a]`?  Magic.
 
-So let's take a *completely useless digressing* and see if we can
+So let's make a completely useless digression and see if we can
 gain some insight into the details of the List monad.  Let's choose
 type constructor that we can peer into, using some of the technology
 we built up so laboriously during the first half of the course.  I'm
@@ -230,10 +234,12 @@ Sigh.  Ocaml won't show us our own list.  So we have to choose an `f`
 and a `z` that will turn our hand-crafted lists into standard Ocaml
 lists, so that they will print out.
 
+<pre>
 # let cons h t = h :: t;;  (* Ocaml is stupid about :: *)
 # l'_bind (fun f z -> f 1 (f 2 z)) 
           (fun i -> fun f z -> f i (f (i+1) z)) cons [];;
 - : int list = [1; 2; 2; 3]
+</pre>
 
 Ta da!
 
@@ -304,3 +310,6 @@ versa.  The connections will be expecially relevant when we consider
 indefinites and Hamblin semantics on the linguistic side, and
 non-determinism on the list monad side.
 
+Refunctionalizing zippers
+-------------------------
+