X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=zipper-lists-continuations.mdwn;h=9ef23c250e4d3c71affbb3a0d40ce72ad156e51c;hp=edc3359d66015d9a0547d02ba7b35c644ff726cf;hb=1758d3493aeb5a8ab805b6cfea11080f72792978;hpb=789245157230b7010000b0ce3290d45bd5a9d8fa

diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
index edc3359d..9ef23c25 100644
--- a/zipper-lists-continuations.mdwn
+++ b/zipper-lists-continuations.mdwn
@@ -73,7 +73,7 @@ The **State Monad** is similar.  Once we've decided to use the following type co
 
 Then our unit is naturally:
 
-    let s_unit (x : 'a) : ('a state) = fun (s : store) -> (x, s)
+    let s_unit (a : 'a) : ('a state) = fun (s : store) -> (a, s)
 
 And we can reason our way to the bind function in a way similar to the reasoning given above. First, we need to apply `f` to the contents of the `u` box:
 
@@ -100,7 +100,7 @@ Our other familiar monad is the **List Monad**, which we were told
 looks like this:
 
     type 'a list = ['a];;
-    l_unit (x : 'a) = [x];;
+    l_unit (a : 'a) = [a];;
     l_bind u f = List.concat (List.map f u);;
 
 Recall that `List.map` take a function and a list and returns the
@@ -167,7 +167,7 @@ general than an ordinary OCaml list, but we'll see how to map them
 into OCaml lists soon.  We don't need to fully grasp the role of the `'b`'s
 in order to proceed to build a monad:
 
-    l'_unit (x : 'a) : ('a, 'b) list = fun x -> fun f z -> f x z
+    l'_unit (a : 'a) : ('a, 'b) list = fun a -> fun f z -> f a z
 
 No problem.  Arriving at bind is a little more complicated, but
 exactly the same principles apply, you just have to be careful and
@@ -219,11 +219,48 @@ Here's a way to persuade yourself that it will have the right behavior. First, i
 
 Now let's think about what this does. It's a wrapper around `u`. In order to behave as the list which is the result of mapping `f` over each element of `u`, and then joining (`concat`ing) the results, this wrapper would have to accept arguments `k` and `z` and fold them in just the same way that the list which is the result of mapping `f` and then joining the results would fold them. Will it?
 
-... MORE...
+Suppose we have a list' whose contents are `[1; 2; 4; 8]`---that is, our list' will be `fun f z -> f 1 (f 2 (f 4 (f 8 z)))`. We call that list' `u`. Suppose we also have a function `f` that for each `int` we give it, gives back a list of the divisors of that `int` that are greater than 1. Intuitively, then, binding `u` to `f` should give us:
 
+	concat (map f u) =
+	concat [[]; [2]; [2; 4]; [2; 4; 8]] =
+	[2; 2; 4; 2; 4; 8]
 
-Our theory is that this monad should be capable of exactly
-replicating the behavior of the standard List monad.  Let's test:
+Or rather, it should give us a list' version of that, which takes a function `k` and value `z` as arguments, and returns the right fold of `k` and `z` over those elements. What does our formula
+
+      fun k z -> u (fun a b -> f a k b) z
+	
+do? Well, for each element `a` in `u`, it applies `f` to that `a`, getting one of the lists:
+
+	[]
+	[2]
+	[2; 4]
+	[2; 4; 8]
+
+(or rather, their list' versions). Then it takes the accumulated result `b` of previous steps in the fold, and it folds `k` and `b` over the list generated by `f a`. The result of doing so is passed on to the next step as the accumulated result so far.
+
+So if, for example, we let `k` be `+` and `z` be `0`, then the computation would proceed:
+
+	0 ==>
+	right-fold + and 0 over [2; 4; 8] = 2+4+8+0 ==>
+	right-fold + and 2+4+8+0 over [2; 4] = 2+4+2+4+8+0 ==>
+	right-fold + and 2+4+2+4+8+0 over [2] = 2+2+4+2+4+8+0 ==>
+	right-fold + and 2+2+4+2+4+8+0 over [] = 2+2+4+2+4+8+0
+
+which indeed is the result of right-folding + and 0 over `[2; 2; 4; 2; 4; 8]`. If you trace through how this works, you should be able to persuade yourself that our formula:
+
+      fun k z -> u (fun a b -> f a k b) z
+
+will deliver just the same folds, for arbitrary choices of `k` and `z` (with the right types), and arbitrary list's `u` and appropriately-typed `f`s, as
+
+	fun k z -> List.fold_right k (concat (map f u)) z
+
+would.
+
+For future reference, we might make two eta-reductions to our formula, so that we have instead:
+
+      let l'_bind = fun k -> u (fun a -> f a k);;
+
+Let's make some more tests:
 
 
     l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3]
@@ -262,7 +299,7 @@ generalized quantifier `fun pred -> pred j` of type `(e -> t) -> t`.
 Let's write a general function that will map individuals into their
 corresponding generalized quantifier:
 
-   gqize (x : e) = fun (p : e -> t) -> p x
+   gqize (a : e) = fun (p : e -> t) -> p a
 
 This function wraps up an individual in a fancy box.  That is to say,
 we are in the presence of a monad.  The type constructor, the unit and
@@ -271,16 +308,16 @@ belabor the construction of the bind function, the derivation is
 similar to the List monad just given:
 
 	type 'a continuation = ('a -> 'b) -> 'b
-	c_unit (x : 'a) = fun (p : 'a -> 'b) -> p x
+	c_unit (a : 'a) = fun (p : 'a -> 'b) -> p a
 	c_bind (u : ('a -> 'b) -> 'b) (f : 'a -> ('c -> 'd) -> 'd) : ('c -> 'd) -> 'd =
-	  fun (k : 'a -> 'b) -> u (fun (x : 'a) -> f x k)
+	  fun (k : 'a -> 'b) -> u (fun (a : 'a) -> f a k)
 
 How similar is it to the List monad?  Let's examine the type
 constructor and the terms from the list monad derived above:
 
     type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
-    l'_unit x = fun f -> f x                 
-    l'_bind u f = fun k -> u (fun x -> f x k)
+    l'_unit a = fun f -> f a                 
+    l'_bind u f = fun k -> u (fun a -> f a k)
 
 (We performed a sneaky but valid eta reduction in the unit term.)