From ba3453bf9e8df1a8bc0abf42727cc1a3fcda9540 Mon Sep 17 00:00:00 2001
From: Chris Barker <barker@omega.(none)>
Date: Fri, 26 Nov 2010 23:42:40 -0500
Subject: [PATCH] edits

---
 zipper-lists-continuations.mdwn | 56 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)

diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
index d13dc353..8c052f0e 100644
--- a/zipper-lists-continuations.mdwn
+++ b/zipper-lists-continuations.mdwn
@@ -248,3 +248,59 @@ To bad this digression, though it ties together various
 elements of the course, has *no relevance whatsoever* to the topic of
 continuations.
 
+Montague's PTQ treatment of DPs as generalized quantifiers
+----------------------------------------------------------
+
+We've hinted that Montague's treatment of DPs as generalized
+quantifiers embodies the spirit of continuations (see de Groote 2001,
+Barker 2002 for lengthy discussion).  Let's see why.  
+
+First, we'll need a type constructor.  As you probably know, 
+Montague replaced individual-denoting determiner phrases (with type `e`)
+with generalized quantifiers (with [extensional] type `(e -> t) -> t`.
+In particular, the denotation of a proper name like *John*, which
+might originally denote a object `j` of type `e`, came to denote a
+generalized quantifier `fun pred -> pred j` of type `(e -> t) -> t`.
+Let's write a general function that will map individuals into their
+corresponding generalized quantifier:
+
+   gqize (x:e) = fun (p:e->t) -> p x
+
+This function wraps up an individual in a fancy 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 I won't
+belabor the construction of the bind function, the derivation is
+similar to the List monad just given:
+
+   type 'a continuation = ('a -> 'b) -> 'b
+   c_unit (x:'a) = fun (p:'a -> 'b) -> p x
+   c_bind (u:('a -> 'b) -> 'b) (f: 'a -> ('c -> 'd) -> 'd): ('c -> 'd) -> 'd =
+     fun (k:'a -> 'b) -> u (fun (x:'a) -> f x k)
+
+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 x = fun f -> f x                 
+    l'_bind u f = fun k -> u (fun x -> f x k)
+
+(I performed a sneaky but valid eta reduction in the unit term.)
+
+The unit and the bind for the Montague continuation monad and the
+homemade List monad are the same terms!  In other words, the behavior
+of the List monad and the behavior of the continuations monad are
+parallel in a deep sense.  To emphasize the parallel, we can
+instantiate the type of the list' monad using the Ocaml list type:
+
+    type 'a c_list = ('a -> 'a list) -> 'a list
+    let c_list_unit x = fun f -> f x;;
+    let c_list_bind u f = fun k -> u (fun x -> f x k);;
+
+Have we really discovered that lists are secretly continuations?
+Or have we merely found a way of simulating lists using list
+continuations?  Both perspectives are valid, and we can use our
+intuitions about the list monad to understand continuations, and vice
+versa.  The connections will be expecially relevant when we consider 
+indefinites and Hamblin semantics on the linguistic side, and
+non-determinism on the list monad side.
+
-- 
2.11.0