author Chris Barker Sun, 28 Nov 2010 18:50:02 +0000 (13:50 -0500) committer Chris Barker Sun, 28 Nov 2010 18:50:02 +0000 (13:50 -0500)

index ab9eee7..958d61d 100644 (file)
@@ -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,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
-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