From 8ad0a5c44c8193ce959dba87fa1f53b819dae178 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 30 Nov 2010 16:10:35 -0500 Subject: [PATCH] week11 tweaks Signed-off-by: Jim Pryor --- list_monad_as_continuation_monad.mdwn | 64 +++++++++++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/list_monad_as_continuation_monad.mdwn b/list_monad_as_continuation_monad.mdwn index aa167a4b..904debb3 100644 --- a/list_monad_as_continuation_monad.mdwn +++ b/list_monad_as_continuation_monad.mdwn @@ -1,3 +1,4 @@ +[[!toc]] Rethinking the list monad @@ -301,3 +302,66 @@ lists, so that they will print out. Ta da! + +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 (a : e) = fun (p : e -> t) -> p a + +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 +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) + +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 + l'_bind u f = fun k -> u (fun a -> f a k) + +(We 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. + +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 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 +to monads that can be understood in terms of continuations? + + -- 2.11.0