X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=zipper-lists-continuations.mdwn;h=637f54d18e2058d326f030188f93827e325c1632;hp=d13dc353d71e06e2aaa4446771ddf5df21360f2f;hb=1237fdc391dbd7d5dc380537211369b0878a2f1b;hpb=fa3fcd726119256a230682b5125180daefd11235 diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn index d13dc353..637f54d1 100644 --- a/zipper-lists-continuations.mdwn +++ b/zipper-lists-continuations.mdwn @@ -5,15 +5,13 @@ continuation monad. The three approches are: -* Rethinking the list monad; -* Montague's PTQ treatment of DPs as generalized quantifiers; and -* Refunctionalizing zippers (Shan: zippers are defunctionalized continuations); +[[!toc]] Rethinking the list monad ------------------------- To construct a monad, the key element is to settle on a type -constructor, and the monad naturally follows from that. I'll remind +constructor, and the monad naturally follows from that. We'll remind you of some examples of how monads follow from the type constructor in a moment. This will involve some review of familair material, but it's worth doing for two reasons: it will set up a pattern for the new @@ -28,10 +26,10 @@ constructor is then we can deduce the unit and the bind: - runit x:'a -> 'a reader = fun (e:env) -> x + r_unit x:'a -> 'a reader = fun (e:env) -> x Since the type of an `'a reader` is `fun e:env -> 'a` (by definition), -the type of the `runit` function is `'a -> e:env -> 'a`, which is a +the type of the `r_unit` function is `'a -> e:env -> 'a`, which is a specific case of the type of the *K* combinator. So it makes sense that *K* is the unit for the reader monad. @@ -45,24 +43,30 @@ We can deduce the correct `bind` function as follows: We have to open up the `u` box and get out the `'a` object in order to feed it to `f`. Since `u` is a function from environments to -objects of type `'a`, we'll have +objects of type `'a`, the way we open a box in this monad is +by applying it to an environment: .... f (u e) ... This subexpression types to `'b reader`, which is good. The only -problem is that we don't have an `e`, so we have to abstract over that -variable: +problem is that we invented an environment `e` that we didn't already have , +so we have to abstract over that variable to balance the books: fun e -> f (u e) ... This types to `env -> 'b reader`, but we want to end up with `env -> -'b`. The easiest way to turn a 'b reader into a 'b is to apply it to +'b`. Once again, the easiest way to turn a `'b reader` into a `'b` is to apply it to an environment. So we end up as follows: r_bind (u:'a reader) (f:'a -> 'b reader):('b reader) = f (u e) e And we're done. +[This bind is a simplified version of the careful `let a = u e in ...` +constructions we provided in earlier lectures. We use the simplified +versions here in order to emphasize similarities of structure across +monads; the official bind is still the one with the plethora of `let`'s.] + The **State Monad** is similar. We somehow intuit that we want to use the following type constructor: @@ -117,14 +121,14 @@ And sure enough, But where is the reasoning that led us to this unit and bind? And what is the type `['a]`? Magic. -So let's take a *completely useless digressing* and see if we can -gain some insight into the details of the List monad. Let's choose -type constructor that we can peer into, using some of the technology -we built up so laboriously during the first half of the course. I'm -going to use type 3 lists, partly because I know they'll give the -result I want, but also because they're my favorite. These were the -lists that made lists look like Church numerals with extra bits -embdded in them: +So let's indulge ourselves in a completely useless digression and see +if we can gain some insight into the details of the List monad. Let's +choose type constructor that we can peer into, using some of the +technology we built up so laboriously during the first half of the +course. We're going to use type 3 lists, partly because I know +they'll give the result I want, but also because they're the coolest. +These were the lists that made lists look like Church numerals with +extra bits embdded in them: empty list: fun f z -> z list with one element: fun f z -> f 1 z @@ -230,10 +234,12 @@ Sigh. Ocaml won't show us our own list. So we have to choose an `f` and a `z` that will turn our hand-crafted lists into standard Ocaml lists, so that they will print out. +
 # let cons h t = h :: t;;  (* Ocaml is stupid about :: *)
 # l'_bind (fun f z -> f 1 (f 2 z)) 
           (fun i -> fun f z -> f i (f (i+1) z)) cons [];;
 - : int list = [1; 2; 2; 3]
+
Ta da! @@ -248,3 +254,62 @@ 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 we 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) + +(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. 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. + +Refunctionalizing zippers +------------------------- +