edits

[lambda.git] / zipper-lists-continuations.mdwn

diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
index ab9eee7..958d61d 100644 (file)
--- 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
 
 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 ... ) ...
 
 
        ... u (fun (a : 'a) (b : 'b) -> ... f a ... ) ...
 


@@ -329,19 +330,28 @@ corresponding generalized quantifier:
 
    gqize (a : e) = fun (p : e -> t) -> p a
 
 
    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
 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)
 
 
        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                 
 
     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
 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
 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