zipper-lists-contin s/x/a/
[lambda.git] / zipper-lists-continuations.mdwn
index 2e84616..9ef23c2 100644 (file)
@@ -73,7 +73,7 @@ The **State Monad** is similar.  Once we've decided to use the following type co
 
 Then our unit is naturally:
 
 
 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:
 
 
 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];;
 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
     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:
 
 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
 
 No problem.  Arriving at bind is a little more complicated, but
 exactly the same principles apply, you just have to be careful and
@@ -299,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:
 
 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
 
 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
@@ -308,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
 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 =
        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
 
 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.)
 
 
 (We performed a sneaky but valid eta reduction in the unit term.)