X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=zipper-lists-continuations.mdwn;h=7687e657bb60270433c21f3c9b33928d5e41a8c4;hp=ab9eee7ce9f33ea76ee54ea9bda36057680468bd;hb=3b0ddcf333b1c0b05d119c92627a2713b467db82;hpb=0a9b2c5fb1adfa3b87e95fcbf26ee79d57ae7466
diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
index ab9eee7c..7687e657 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,15 +367,12 @@ 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
to monads that can be understood in terms of continuations?
-Refunctionalizing zippers
--------------------------
-
Manipulating trees with monads
------------------------------
@@ -758,3 +765,151 @@ 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.
+
+
+Refunctionalizing zippers: from lists to 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:
+
+
+t1 "abSe" ~~> "ababe"
+
+
+
+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'):
+
+
+ t1 "aSbS"
+ *
+~~> t1 "aabS"
+ *
+~~> "aabaab"
+
+
+versus
+
+
+ t1 "aSbS"
+ *
+~~> t1 "aSbaSb"
+ *
+~~> t1 "aabaSb"
+ *
+~~> "aabaaabab"
+
+
+versus
+
+
+ t1 "aSbS"
+ *
+~~> t1 "aSbaSb"
+ *
+~~> t1 "aSbaaSbab"
+ *
+~~> t1 "aSbaaaSbaabab"
+ *
+~~> ...
+
+
+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.
+
+
+type 'a list_zipper = ('a list) * ('a list);;
+
+let rec t1 (z:char list_zipper) =
+ match z with (sofar, []) -> List.rev(sofar) (* Done! *)
+ | (sofar, 'S'::rest) -> t1 ((List.append sofar sofar), rest)
+ | (sofar, fst::rest) -> t1 (fst::sofar, rest);; (* Move zipper *)
+
+# 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']
+
+
+Note that this implementation enforces the evaluate-leftmost rule.
+Task 1 completed.
+
+One way to see exactly what is going on is to watch the zipper in
+action by tracing the execution of `t1`. By using the `#trace`
+directive in the Ocaml interpreter, the system will print out the
+arguments to `t1` each time it is (recurcively) called:
+
+
+# #trace t1;;
+t1 is now traced.
+# t1 ([], ['a'; 'b'; 'S'; 'e']);;
+t1 <-- ([], ['a'; 'b'; 'S'; 'e'])
+t1 <-- (['a'], ['b'; 'S'; 'e'])
+t1 <-- (['b'; 'a'], ['S'; 'e'])
+t1 <-- (['b'; 'a'; 'b'; 'a'], ['e'])
+t1 <-- (['e'; 'b'; 'a'; 'b'; 'a'], [])
+t1 --> ['a'; 'b'; 'a'; 'b'; 'e']
+t1 --> ['a'; 'b'; 'a'; 'b'; 'e']
+t1 --> ['a'; 'b'; 'a'; 'b'; 'e']
+t1 --> ['a'; 'b'; 'a'; 'b'; 'e']
+t1 --> ['a'; 'b'; 'a'; 'b'; 'e']
+- : char list = ['a'; 'b'; 'a'; 'b'; 'e']
+
+
+The nice thing about computations involving lists is that it's so easy
+to visualize them as a data structure. Eventually, we want to get to
+a place where we can talk about more abstract computations. In order
+to get there, we'll first do the exact same thing we just did with
+concrete zipper using procedures.
+
+Think of a list as a procedural recipe: `['a'; 'b'; 'c']` means (1)
+start with the empty list `[]`; (2) make a new list whose first
+element is 'c' and whose tail is the list construted in the previous
+step; (3) make a new list whose first element is 'b' and whose tail is
+the list constructed in the previous step; and (4) make a new list
+whose first element is 'a' and whose tail is the list constructed in
+the previous step.
+
+What is the type of each of these steps? Well, it will be a function
+from the result of the previous step (a list) to a new list: it will
+be a function of type `char list -> char list`. We'll call each step
+a **continuation** of the recipe. So in this context, a continuation
+is a function of type `char list -> char list`.
+
+This means that we can now represent the sofar part of our zipper--the
+part we've already unzipped--as a continuation, a function describing
+how to finish building the list:
+
+
+let rec t1c (l: char list) (c: (char list) -> (char list)) =
+ match l with [] -> c []
+ | 'S'::rest -> t1c rest (fun x -> c (c x))
+ | a::rest -> t1c rest (fun x -> List.append (c x) [a]);;
+
+# t1c ['a'; 'b'; 'S'] (fun x -> x);;
+- : char list = ['a'; 'b'; 'a'; 'b']
+
+# t1c ['a'; 'S'; 'b'; 'S'] (fun x -> x);;
+- : char list = ['a'; 'a'; 'b'; 'a'; 'a'; 'b']
+
+
+Note that we don't need to do any reversing.
+