If zippers are continuations reified (defuntionalized), then one route
to continuations is to re-functionalize a zipper. Then the
concreteness and understandability of the zipper provides a way of
-understanding and equivalent treatment using continuations.
+understanding an equivalent treatment using continuations.
Let's work with lists of `char`s for a change. To maximize readability, we'll
indulge in an abbreviatory convention that "abSd" abbreviates the
Expected behavior:
-<pre>
-t "abSd" ~~> "ababd"
-</pre>
+ t "abSd" ~~> "ababd"
In linguistic terms, this is a kind of anaphora
Note that it matters which 'S' you target first (the position of the *
indicates the targeted 'S'):
-<pre>
- t "aSbS"
- *
-~~> t "aabS"
- *
-~~> "aabaab"
-</pre>
+ t "aSbS"
+ *
+ ~~> t "aabS"
+ *
+ ~~> "aabaab"
versus
-<pre>
- t "aSbS"
- *
-~~> t "aSbaSb"
- *
-~~> t "aabaSb"
- *
-~~> "aabaaabab"
-</pre>
+ t "aSbS"
+ *
+ ~~> t "aSbaSb"
+ *
+ ~~> t "aabaSb"
+ *
+ ~~> "aabaaabab"
versus
-<pre>
- t "aSbS"
- *
-~~> t "aSbaSb"
- *
-~~> t "aSbaaSbab"
- *
-~~> t "aSbaaaSbaabab"
- *
-~~> ...
-</pre>
+ t "aSbS"
+ *
+ ~~> t "aSbaSb"
+ *
+ ~~> t "aSbaaSbab"
+ *
+ ~~> t "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
`tz` (for task with zippers), which accomplishes the task by mapping a
`char list zipper` to a `char list`. We'll call the two parts of the
zipper `unzipped` and `zipped`; we start with a fully zipped list, and
-move elements to the zipped part by pulling the zipper down until the
+move elements to the unzipped part by pulling the zipper down until the
entire list has been unzipped (and so the zipped half of the zipper is empty).
-<pre>
-type 'a list_zipper = ('a list) * ('a list);;
-
-let rec tz (z:char list_zipper) =
- match z with (unzipped, []) -> List.rev(unzipped) (* Done! *)
- | (unzipped, 'S'::zipped) -> tz ((List.append unzipped unzipped), zipped)
- | (unzipped, target::zipped) -> tz (target::unzipped, zipped);; (* Pull zipper *)
-
-# tz ([], ['a'; 'b'; 'S'; 'd']);;
-- : char list = ['a'; 'b'; 'a'; 'b'; 'd']
-
-# tz ([], ['a'; 'S'; 'b'; 'S']);;
-- : char list = ['a'; 'a'; 'b'; 'a'; 'a'; 'b']
-</pre>
+ type 'a list_zipper = ('a list) * ('a list);;
+
+ let rec tz (z : char list_zipper) =
+ match z with
+ | (unzipped, []) -> List.rev(unzipped) (* Done! *)
+ | (unzipped, 'S'::zipped) -> tz ((List.append unzipped unzipped), zipped)
+ | (unzipped, target::zipped) -> tz (target::unzipped, zipped);; (* Pull zipper *)
+
+ # tz ([], ['a'; 'b'; 'S'; 'd']);;
+ - : char list = ['a'; 'b'; 'a'; 'b'; 'd']
+
+ # tz ([], ['a'; 'S'; 'b'; 'S']);;
+ - : char list = ['a'; 'a'; 'b'; 'a'; 'a'; 'b']
Note that this implementation enforces the evaluate-leftmost rule.
Task completed.
One way to see exactly what is going on is to watch the zipper in
action by tracing the execution of `tz`. By using the `#trace`
-directive in the Ocaml interpreter, the system will print out the
+directive in the OCaml interpreter, the system will print out the
arguments to `tz` each time it is (recurcively) called. Note that the
lines with left-facing arrows (`<--`) show (recursive) calls to `tz`,
giving the value of its argument (a zipper), and the lines with
right-facing arrows (`-->`) show the output of each recursive call, a
-simple list.
-
-<pre>
-# #trace tz;;
-t1 is now traced.
-# tz ([], ['a'; 'b'; 'S'; 'd']);;
-tz <-- ([], ['a'; 'b'; 'S'; 'd'])
-tz <-- (['a'], ['b'; 'S'; 'd']) (* Pull zipper *)
-tz <-- (['b'; 'a'], ['S'; 'd']) (* Pull zipper *)
-tz <-- (['b'; 'a'; 'b'; 'a'], ['d']) (* Special step *)
-tz <-- (['d'; 'b'; 'a'; 'b'; 'a'], []) (* Pull zipper *)
-tz --> ['a'; 'b'; 'a'; 'b'; 'd'] (* Output reversed *)
-tz --> ['a'; 'b'; 'a'; 'b'; 'd']
-tz --> ['a'; 'b'; 'a'; 'b'; 'd']
-tz --> ['a'; 'b'; 'a'; 'b'; 'd']
-tz --> ['a'; 'b'; 'a'; 'b'; 'd']
-- : char list = ['a'; 'b'; 'a'; 'b'; 'd']
-</pre>
+simple list.
+
+ # #trace tz;;
+ t1 is now traced.
+ # tz ([], ['a'; 'b'; 'S'; 'd']);;
+ tz <-- ([], ['a'; 'b'; 'S'; 'd'])
+ tz <-- (['a'], ['b'; 'S'; 'd']) (* Pull zipper *)
+ tz <-- (['b'; 'a'], ['S'; 'd']) (* Pull zipper *)
+ tz <-- (['b'; 'a'; 'b'; 'a'], ['d']) (* Special step *)
+ tz <-- (['d'; 'b'; 'a'; 'b'; 'a'], []) (* Pull zipper *)
+ tz --> ['a'; 'b'; 'a'; 'b'; 'd'] (* Output reversed *)
+ tz --> ['a'; 'b'; 'a'; 'b'; 'd']
+ tz --> ['a'; 'b'; 'a'; 'b'; 'd']
+ tz --> ['a'; 'b'; 'a'; 'b'; 'd']
+ tz --> ['a'; 'b'; 'a'; 'b'; 'd']
+ - : char list = ['a'; 'b'; 'a'; 'b'; 'd']
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'; 'S'; 'd']`
-is the result of the computation `'a'::('b'::('S'::('d'::[])))` (or, in our old
-style, `make_list 'a' (make_list 'b' (make_list 'S' (make_list 'd' empty)))`).
-The recipe for constructing the list goes like this:
-
-<pre>
-(0) Start with the empty list []
-(1) make a new list whose first element is 'd' and whose tail is the list constructed in step (0)
-(2) make a new list whose first element is 'S' and whose tail is the list constructed in step (1)
------------------------------------------
-(3) make a new list whose first element is 'b' and whose tail is the list constructed in step (2)
-(4) make a new list whose first element is 'a' and whose tail is the list constructed in step (3)
-</pre>
+concrete zipper using procedures.
+
+Think of a list as a procedural recipe: `['a'; 'b'; 'S'; 'd']` is the result of
+the computation `'a'::('b'::('S'::('d'::[])))` (or, in our old style,
+`make_list 'a' (make_list 'b' (make_list 'S' (make_list 'd' empty)))`). The
+recipe for constructing the list goes like this:
+
+> (0) Start with the empty list []
+> (1) make a new list whose first element is 'd' and whose tail is the list constructed in step (0)
+> (2) make a new list whose first element is 'S' and whose tail is the list constructed in step (1)
+> -----------------------------------------
+> (3) make a new list whose first element is 'b' and whose tail is the list constructed in step (2)
+> (4) make a new list whose first element is 'a' and whose tail is the list constructed in step (3)
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
(or group of steps) a **continuation** of the recipe. So in this
context, a continuation is a function of type `char list -> char
list`. For instance, the continuation corresponding to the portion of
-the recipe below the horizontal line is the function `fun (tail:char
+the recipe below the horizontal line is the function `fun (tail : char
list) -> 'a'::('b'::tail)`.
This means that we can now represent the unzipped part of our
zipper---the part we've already unzipped---as a continuation: a function
-describing how to finish building the list. We'll write a new
+describing how to finish building a list. We'll write a new
function, `tc` (for task with continuations), that will take an input
list (not a zipper!) and a continuation and return a processed list.
The structure and the behavior will follow that of `tz` above, with
some small but interesting differences. We've included the orginal
`tz` to facilitate detailed comparison:
-<pre>
-let rec tz (z:char list_zipper) =
- match z with (unzipped, []) -> List.rev(unzipped) (* Done! *)
- | (unzipped, 'S'::zipped) -> tz ((List.append unzipped unzipped), zipped)
- | (unzipped, target::zipped) -> tz (target::unzipped, zipped);; (* Pull zipper *)
-
-let rec tc (l: char list) (c: (char list) -> (char list)) =
- match l with [] -> List.rev (c [])
- | 'S'::zipped -> tc zipped (fun x -> c (c x))
- | target::zipped -> tc zipped (fun x -> target::(c x));;
-
-# tc ['a'; 'b'; 'S'; 'd'] (fun x -> x);;
-- : char list = ['a'; 'b'; 'a'; 'b']
-
-# tc ['a'; 'S'; 'b'; 'S'] (fun x -> x);;
-- : char list = ['a'; 'a'; 'b'; 'a'; 'a'; 'b']
-</pre>
+ let rec tz (z : char list_zipper) =
+ match z with
+ | (unzipped, []) -> List.rev(unzipped) (* Done! *)
+ | (unzipped, 'S'::zipped) -> tz ((List.append unzipped unzipped), zipped)
+ | (unzipped, target::zipped) -> tz (target::unzipped, zipped);; (* Pull zipper *)
+
+ let rec tc (l: char list) (c: (char list) -> (char list)) =
+ match l with
+ | [] -> List.rev (c [])
+ | 'S'::zipped -> tc zipped (fun x -> c (c x))
+ | target::zipped -> tc zipped (fun x -> target::(c x));;
+
+ # tc ['a'; 'b'; 'S'; 'd'] (fun x -> x);;
+ - : char list = ['a'; 'b'; 'a'; 'b']
+
+ # tc ['a'; 'S'; 'b'; 'S'] (fun x -> x);;
+ - : char list = ['a'; 'a'; 'b'; 'a'; 'a'; 'b']
To emphasize the parallel, I've re-used the names `zipped` and
`target`. The trace of the procedure will show that these variables
you can see this difference in the fact that in `tz`, we have to glue
together the two instances of `unzipped` with an explicit (and
relatively inefficient) `List.append`.
-In the `tc` version of the task, we simply compose `c` with itself:
+In the `tc` version of the task, we simply compose `c` with itself:
`c o c = fun x -> c (c x)`.
-Why use the identity function as the initial continuation? Well, if
-you have already constructed the initial list `"abSd"`, what's the next
-step in the recipe to produce the desired result, i.e, the very same
-list, `"abSd"`? Clearly, the identity continuation.
+A call `tc ['a'; 'b'; 'S'; 'd']` yields a partially-applied function; it still waits for another argument, a continuation of type `char list -> char list`. We have to give it an "initial continuation" to get started. Here we supply *the identity function* as the initial continuation. Why did we choose that? Well, if
+you have already constructed the initial list `"abSd"`, what's the desired continuation? What's the next step in the recipe to produce the desired result, i.e, the very same list, `"abSd"`? Clearly, the identity function.
A good way to test your understanding is to figure out what the
continuation function `c` must be at the point in the computation when
list task after talking about generalized quantifiers below.
-