X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=from_lists_to_continuations.mdwn;h=170ae5d4e858b5de4eefaec8a8e104f5580e9a42;hp=0b3f4643cbcb890edd85565be664670dc38de7d6;hb=56ec8c944aeb4611b83fceecfe91cfb1dbf54840;hpb=cd3b0839319cccf085142a33c82c32df1bcf69d4
diff --git a/from_lists_to_continuations.mdwn b/from_lists_to_continuations.mdwn
index 0b3f4643..170ae5d4 100644
--- a/from_lists_to_continuations.mdwn
+++ b/from_lists_to_continuations.mdwn
@@ -1,4 +1,3 @@
-
Refunctionalizing zippers: from lists to continuations
------------------------------------------------------
@@ -7,7 +6,7 @@ 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.
-Let's work with lists of chars for a change. To maximize readability, we'll
+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
list `['a'; 'b'; 'S'; 'd']`.
@@ -20,9 +19,7 @@ updated version.
Expected behavior:
-
-t "abSd" ~~> "ababd"
-
+ t "abSd" ~~> "ababd"
In linguistic terms, this is a kind of anaphora
@@ -33,39 +30,33 @@ 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'):
-
- t "aSbS"
- *
-~~> t "aabS"
- *
-~~> "aabaab"
-
+ t "aSbS"
+ *
+ ~~> t "aabS"
+ *
+ ~~> "aabaab"
versus
-
- t "aSbS"
- *
-~~> t "aSbaSb"
- *
-~~> t "aabaSb"
- *
-~~> "aabaaabab"
-
+ t "aSbS"
+ *
+ ~~> t "aSbaSb"
+ *
+ ~~> t "aabaSb"
+ *
+ ~~> "aabaaabab"
versus
-
- t "aSbS"
- *
-~~> t "aSbaSb"
- *
-~~> t "aSbaaSbab"
- *
-~~> t "aSbaaaSbaabab"
- *
-~~> ...
-
+ 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
@@ -76,25 +67,24 @@ guarantees termination, and a final string without any `'S'` in it.
This is a task well-suited to using a zipper. We'll define a function
`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
+`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 zipped down until the
+move elements to the zipped part by pulling the zipper down until the
entire list has been unzipped (and so the zipped half of the zipper is empty).
-
-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']
-
+ 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.
@@ -132,8 +122,8 @@ 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, `makelist a (makelist b (makelist S (makelist c empty)))`).
+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:
@@ -148,13 +138,14 @@ The recipe for constructing the list goes like this:
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`. 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)`.
+(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
+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---the part we've already unzipped---as a continuation: a function
describing how to finish building the 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.
@@ -162,23 +153,23 @@ 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:
-
-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']
-
+ 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
@@ -194,42 +185,44 @@ what the parallel would suggest. The reason is that `unzipped` is a
list, but `c` 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 `List.append`.
+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:
`c o c = fun x -> c (c x)`.
Why use the identity function as the initial continuation? Well, if
-you have already constructed the list "abSd", what's the next step in
-the recipe to produce the desired result (which is the same list,
-"abSd")? Clearly, the identity continuation.
+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 good way to test your understanding is to figure out what the
continuation function `c` must be at the point in the computation when
`tc` is called with the first argument `"Sd"`. Two choices: is it
-`fun x -> a::b::x`, or it is `fun x -> b::a::x`?
-The way to see if you're right is to execute the following
-command and see what happens:
+`fun x -> a::b::x`, or it is `fun x -> b::a::x`? The way to see if
+you're right is to execute the following command and see what happens:
tc ['S'; 'd'] (fun x -> 'a'::'b'::x);;
There are a number of interesting directions we can go with this task.
-The task was chosen because the computation can be viewed as a
+The reason this task was chosen is because it can be viewed as a
simplified picture of a computation using continuations, where `'S'`
plays the role of a control operator with some similarities to what is
-often called `shift`. In the analogy, the list portrays a string of
-functional applications, where `[f1; f2; f3; x]` represents `f1(f2(f3
-x))`. The limitation of the analogy is that it is only possible to
-represent computations in which the applications are always
-right-branching, i.e., the computation `((f1 f2) f3) x` cannot be
-directly represented.
+often called `shift`. In the analogy, the input list portrays a
+sequence of functional applications, where `[f1; f2; f3; x]` represents
+`f1(f2(f3 x))`. The limitation of the analogy is that it is only
+possible to represent computations in which the applications are
+always right-branching, i.e., the computation `((f1 f2) f3) x` cannot
+be directly represented.
One possibile development is that we could add a special symbol `'#'`,
and then the task would be to copy from the target `'S'` only back to
the closest `'#'`. This would allow the task to simulate delimited
-continuations (for right-branching computations).
+continuations with embedded prompts.
+
+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.
+
-The task is well-suited to the list zipper because the list monad has
-an intimate connection with continuations. The following section
-makes this connection. We'll return to the list task after talking
-about generalized quantifiers below.