X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=zipper-lists-continuations.mdwn;h=267015d3b651d3bd076f39bfb0668de2f2ca41c6;hp=ab9eee7ce9f33ea76ee54ea9bda36057680468bd;hb=d30463cb5a4ac07600f4b587249edde28270dfcf;hpb=0a9b2c5fb1adfa3b87e95fcbf26ee79d57ae7466

diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
index ab9eee7c..267015d3 100644
--- a/zipper-lists-continuations.mdwn
+++ b/zipper-lists-continuations.mdwn
@@ -219,7 +219,8 @@ paragraph much easier to follow.]
 
 As usual, we need to unpack the `u` box.  Examine the type of `u`.
 This time, `u` will only deliver up its contents if we give `u` an
-argument that is a function expecting an `'a` and a `'b`. `u` will fold that function over its type `'a` members, and that's how we'll get the `'a`s we need. Thus:
+argument that is a function expecting an `'a` and a `'b`. `u` will 
+fold that function over its type `'a` members, and that's how we'll get the `'a`s we need. Thus:
 
 	... u (fun (a : 'a) (b : 'b) -> ... f a ... ) ...
 
@@ -329,19 +330,28 @@ corresponding generalized quantifier:
 
    gqize (a : e) = fun (p : e -> t) -> p a
 
-This function wraps up an individual in a fancy box.  That is to say,
+This function is what Partee 1987 calls LIFT, and it would be
+reasonable to use it here, but we will avoid that name, given that we
+use that word to refer to other functions.
+
+This function wraps up an individual in a box.  That is to say,
 we are in the presence of a monad.  The type constructor, the unit and
 the bind follow naturally.  We've done this enough times that we won't
 belabor the construction of the bind function, the derivation is
-similar to the List monad just given:
+highly similar to the List monad just given:
 
 	type 'a continuation = ('a -> 'b) -> 'b
 	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 (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:
+Note that `c_bind` is exactly the `gqize` function that Montague used
+to lift individuals into the continuation monad.
+
+That last bit in `c_bind` looks familiar---we just saw something like
+it in the List monad.  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 a = fun f -> f a                 
@@ -357,7 +367,7 @@ parallel in a deep sense.
 Have we really discovered that lists are secretly continuations?  Or
 have we merely found a way of simulating lists using list
 continuations?  Well, strictly speaking, what we have done is shown
-that one particular implementation of lists---the left fold
+that one particular implementation of lists---the right fold
 implementation---gives rise to a continuation monad fairly naturally,
 and that this monad can reproduce the behavior of the standard list
 monad.  But what about other list implementations?  Do they give rise
@@ -758,3 +768,96 @@ called a
 [SearchTree](http://hackage.haskell.org/packages/archive/tree-monad/0.2.1/doc/html/src/Control-Monad-SearchTree.html#SearchTree)
 that is intended to 
 represent non-deterministic computations as a tree.
+
+
+Lists, zippers, continuations
+-----------------------------
+
+Let's work with lists of chars for a change.  To maximize readability, we'll
+indulge in an abbreviatory convention that "abc" abbreviates the
+list `['a'; 'b'; 'c']`.
+
+Task 1: replace each occurrence of 'S' with a copy of the string up to
+that point.  
+
+Expected behavior:
+
+<pre>
+t1 "abSe" ~~> "ababe"
+</pre>   
+
+
+In linguistic terms, this is a kind of anaphora
+resolution, where `'S'` is functioning like an anaphoric element, and
+the preceding string portion is the antecedent.
+
+This deceptively simple task gives rise to some mind-bending complexity.
+Note that it matters which 'S' you target first (the position of the *
+indicates the targeted 'S'):
+
+<pre>
+    t1 "aSbS" 
+         *
+~~> t1 "aabS" 
+           *
+~~> "aabaab"
+<pre>
+
+versus
+
+<pre>
+    t1 "aSbS"
+           *
+~~> t1 "aSbaSb" 
+         *
+~~> t1 "aabaSb"
+            *
+~~> "aabaaabab"
+</pre>   
+
+versus
+
+<pre>
+    t1 "aSbS"
+           *
+~~> t1 "aSbaSb"
+            *
+~~> t1 "aSbaaSbab"
+             *
+~~> t1 "aSbaaaSbaabab"
+              *
+~~> ...
+</pre>
+
+Aparently, this task, as simple as it is, is a form of computation,
+and the order in which the `'S'`s get evaluated can lead to divergent
+behavior.
+
+For now, as usual, we'll agree to always ``evaluate'' the leftmost `'S'`.
+
+This is a task well-suited to using a zipper.  
+
+<pre>
+type 'a list_zipper = ('a list) * ('a list);;
+
+let rec t1 (z:char list_zipper) = 
+    match z with (sofar, []) -> List.rev(sofar)
+               | (sofar, 'S'::rest) -> t1 ((List.append sofar sofar), rest)
+               | (sofar, fst::rest) -> t1 (fst::sofar, rest);;
+
+# t1 ([], ['a'; 'b'; 'S'; 'e']);;
+- : char list = ['a'; 'b'; 'a'; 'b'; 'e']
+
+# t1 ([], ['a'; 'S'; 'b'; 'S']);;
+- : char list = ['a'; 'a'; 'b'; 'a'; 'a'; 'b']
+</pre>
+
+Note that this implementation enforces the evaluate-leftmost rule.
+Task 1 completed.
+
+
+
+
+
+
+