-Refunctionalizing list zippers
-------------------------------
+Refunctionalizing zippers: from lists to continuations
+------------------------------------------------------
If zippers are continuations reified (defuntionalized), then one route
to continuations is to re-functionalize a zipper. Then the
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.
+This task can give rise to considerable complexity.
Note that it matters which 'S' you target first (the position of the *
indicates the targeted 'S'):
*
~~> ...
-Aparently, this task, as simple as it is, is a form of computation,
+Apparently, 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.
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 *)
+ 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']
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
-arguments to `tz` each time it is (recurcively) called. Note that the
+arguments to `tz` each time it is (recursively) 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
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.
+concrete zipper using procedures instead.
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,
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
-(or group of steps) a **continuation** of the recipe. So in this
+(or group of steps) a **continuation** of the previous steps. 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
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
+zipper as a continuation: a function
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 `k` (it's conventional to use `k` for continuation variables) and return a processed list.
# tc ['a'; 'S'; 'b'; 'S'] (fun tail -> tail);;
- : char list = ['a'; 'a'; 'b'; 'a'; 'a'; 'b']
-To emphasize the parallel, I've re-used the names `zipped` and
+To emphasize the parallel, we've re-used the names `zipped` and
`target`. The trace of the procedure will show that these variables
take on the same values in the same series of steps as they did during
the execution of `tz` above. There will once again be one initial and
four recursive calls to `tc`, and `zipped` will take on the values
`"bSd"`, `"Sd"`, `"d"`, and `""` (and, once again, on the final call,
-the first `match` clause will fire, so the the variable `zipper` will
+the first `match` clause will fire, so the the variable `zipped` will
not be instantiated).
-I have not called the functional argument `unzipped`, although that is
+We have not called the functional argument `unzipped`, although that is
what the parallel would suggest. The reason is that `unzipped` is a
list, but `k` is a function. That's the most crucial difference, the
point of the excercise, and it should be emphasized. For instance,
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`.
+together the two instances of `unzipped` with an explicit (and,
+computationally speaking, relatively inefficient) `List.append`.
In the `tc` version of the task, we simply compose `k` with itself:
`k o k = fun tail -> k (k tail)`.
The reason the task is well-suited to the list zipper is in part
because the list monad has an intimate connection with continuations.
-The following section explores this connection. We'll return to the
-list task after talking about generalized quantifiers below.
+We'll explore this next.