From: Chris Date: Wed, 13 May 2015 17:04:45 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=1efbaa05ade48388ad996f60091c9b6f8bc58c1d;hp=8e42213815ea8a2e0013aa4039a5d9bc44697425 edits --- diff --git a/topics/_week14_continuations.mdwn b/topics/_week14_continuations.mdwn index 0b99065f..42f2c118 100644 --- a/topics/_week14_continuations.mdwn +++ b/topics/_week14_continuations.mdwn @@ -65,7 +65,7 @@ We have to lift each functor (+) and each object (e.g., "b") into the monad using mid (`⇧`), then combine them using monadic function application, where - ¢ mf mx = \k -> mf (\f -> mx (\a -> k(f x))) + ¢ M N = \k -> M (\f -> N (\a -> k(f x))) for the continuation monad. @@ -73,17 +73,16 @@ The way in which we extract a value from a continuation box is by applying it to a continuation; often, it is convenient to supply the trivial continuation, the identity function \k.k = I. So in fact, - t1 = mt1 I + t1 = mt1 I That is, the original computation is the monadic version applied to the trivial continuation. -We can now imagine replacing the third element ("c") with a shifty -operator. We would like to replace just the one element, and we will -do just that in a moment; but in order to simulate the original task, -we'll have to take a different strategy initially. We'll start by -imagining a shift operator that combined direction with the tail of -the list, like this: +We can now add a shifty operator. We would like to replace just the +one element, and we will do just that in a moment; but in order to +simulate the original task, we'll have to take a different strategy +initially. We'll start by imagining a shift operator that combined +direction with the tail of the list, like this: mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d)) @@ -96,7 +95,7 @@ and a string continuation k of type [Char] -> [Char]. Since u is the the argument to shift, it represents the tail of the list after the shift operator. Then k is the continuation of the expression headed by `shift`. So in order to execute the task, shift needs to invoke k -twice. +twice. The expression `\s.k(ks)` is just the composition of k with itself. mt2 I == "ababd" @@ -118,19 +117,26 @@ For a reset operator #, we can have # u k = k(u(\k.k)) -- ex.: ab#deSf ~~> abdedef +The reset operator executes the remainder of the list separately, by +giving it the trivial continuation (\k.k), then feeds the result to +the continuation corresponding to the position of the reset. + So the continuation monad solves the list task using continuations in a way that conforms to our by-now familiar strategy of lifting a computation into a monad, and then writing a few key functions (shift, reset) that exploit the power of the monad. +## Generalizing to the tree doubling task + Now we should consider what happens when we write a shift operator that takes the place of a single letter. mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d)) mt4 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ shift' ¢ ⇧d)) -Instead of mt2, we have mt4. So now the type of "c" (a boxed string, -type M[Char]) is the same as the type of the new shift operator, shift'. +Instead of mt2 (copied from above), we have mt4. So now the type of a +leaf (a boxed string, type M[Char]) is the same as the type of the new +shift operator, shift'. shift' = \k.k(k"") @@ -179,6 +185,7 @@ Let's go back to a simple one-shift example, "aSc". Let's trace what the shift' operator sees as its argument k by replacing ⇧ and ¢ with their definitions: +
       ⇧+ ¢ ⇧a ¢ (⇧+ ¢ shift' ¢ ⇧c) I
    = \k.⇧+(\f.⇧a(\x.k(fx))) ¢ (⇧+ ¢ shift' ¢ ⇧c) I
    = \k.(\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(\x.k(fx))) I
@@ -199,106 +206,14 @@ their definitions:
    ~~> shift(\x.⇧c(\x'.(+a)((+x)x'))))
    = shift(\x.(\k.kc)(\x'.(+a)((+x)x'))))
    ~~> shift(\x.(+a)((+x)c))
+
So now we see what the argument of shift will be: a function k from strings x to the string asc. So shift k will be k(k "") = aacc. Ok, this is ridiculous. We need a way to get ahead of this deluge of -lambda conversion. We'll adapt the notational strategy developed in -Barker and Shan 2014: - -Instead of writing - - \k.g(kf): (α -> ρ) -> ρ - -we'll write - - g[] ρ - --- : --- - f α - -Then - [] - mid(x) = -- - x - -and - - g[] ρ h[] ρ g[h[]] ρ - --- : ---- ¢ --- : --- = ------ : --- - f α->β x α fx β - -Here's the justification: - - (\FXk.F(\f.X(\x.k(fx)))) (\k.g(kf)) (\k.h(kx)) - ~~> (\Xk.(\k.g(kf))(\f.X(\x.k(fx)))) (\k.h(kx)) - ~~> \k.(\k.g(kf))(\f.(\k.h(kx))(\x.k(fx))) - ~~> \k.g((\f.(\k.h(kx))(\x.k(fx)))f) - ~~> \k.g((\k.h(kx))(\x.k(fx))) - ~~> \k.g(h(\x.k(fx))x) - ~~> \k.g(h(k(fx))) - -Then - (\ks.k(ks))[] - shift = \k.k(k("")) = ------------- - "" - -Let 2 == \ks.k(ks). - -so aSc lifted into the monad is - - [] 2[] [] - -- ¢ ( --- ¢ --- ) = - a "" c - -First, we need map2 instead of map1. Second, the type of the shift -operator will be a string continuation, rather than a function from -string continuations to string continuations. - -(\k.k(k1))(\s.(\k.k(k2))(\r.sr)) -(\k.k(k1))(\s.(\r.sr)((\r.sr)2)) -(\k.k(k1))(\s.(\r.sr)(s2)) -(\k.k(k1))(\s.s(s2)) -(\s.s(s2))((\s.s(s2))1) -(\s.s(s2))(1(12)) -(1(12))((1(12)2)) - - - - - -But here's the interesting part: from the point of view of the shift -operator, the continuation that it will be fed will be the entire rest -of the computation. This includes not only what has come before, but -what will come after it as well. That means when the continuation is -doubled (self-composed), the result duplicates not only the prefix -`(ab ~~> abab)`, but also the suffix `(d ~~> dd)`. In some sense, then, -continuations allow functions to see into the future! - -What do you expect will be the result of executing "aScSe" under the -second perspective? The answer to this question is not determined by -the informal specification of the task that we've been using, since -under the new perspective, we're copying complete (bi-directional) -contexts rather than just left contexts. - -It might be natural to assume that what execution does is choose an S, -and double its context, temporarily treating all other shift operators -as dumb letters, then choosing a remaining S to execute. If that was -our interpreation of the task, then no string with more than one S -would ever terminate, since the number S's after each reduction step -would always be 2(n-1), where n is the number before reduction. - -But there is another equally natural way to answer the question. -Assume the leftmost S is executed first. What will the value of its -continuation k be? It will be a function that maps a string s to the -result of computing `ascSe`, which will be `ascascee`. So `k(k "")` -will be `k(acacee)`, which will result in `a(acacee)ca(acacee)cee` -(the parentheses are added to show stages in the construction of the -final result). - -So the continuation monad behaves in a way that we expect a -continuation to behave. But where did the continuation monad come -from? Let's consider some ways of deriving the continuation monad. +lambda conversion. We'll see how to understand what is going on +when we talk about quantifier raising in the next lecture. ## Viewing Montague's PTQ as CPS @@ -325,80 +240,6 @@ quantificational DPs, as in *John and no dog left*. Then generalized quantifier corresponding to the proper name *John* is the quantifier `\k.kj`. -At this point, we have a type for our Kliesli arrow and a value for -our mid. Given some result type (such as `t` in the Montague application), - - α ==> (α -> ρ) -> ρ - ⇧a = \k.ka - -It remains only to find a suitable value for bind. Montague didn't -provide one, but it's easy to find: - - bind :: Mα -> (α -> Mβ) -> Mβ - -given variables of the following types - - u :: Mα == (α -> ρ) -> ρ - f :: α -> Mβ - k :: β -> ρ - x :: α - -We have - - bind u f = \k.u(\x.fxk) - -Let's carefully make sure that this types out: - - bind u f = \k. u (\x . f x k) - -------- -- - α -> Mβ α - ------------ ------ - Mβ β -> ρ - -- -------------------- - α ρ - ------------- ------------------------ - (α -> ρ) -> ρ α -> ρ - --------------------------------- - ρ - ----------------------- - (β -> ρ) -> ρ - -Yep! - -Is there any other way of building a bind operator? Well, the -challenge is getting hold of the "a" that is buried inside of `u`. -In the Reader monad, we could get at the a inside of the box by -applying the box to an environment. In the State monad, we could get -at the a by applying to box to a state and deconstructing the -resulting pair. In the continuation case, the only way to do it is to -apply the boxed a (i.e., u) to a function that takes an a as an -argument. That means that f must be invoked inside the scope of the -functional argument to u. So we've deduced the structure - - ... u (\x. ... f x ...) ... - -At this point, in order to provide u with an argument of the -appropriate type, the argument must not only take objects of type -α as an argument, it must return a result of type ρ. That means that -we must apply fx to an object of type β -> ρ. We can hypothesize such -an object, as long as we eliminate that hypothesis later (by binding -it), and we have the complete bind operation. - -The way in which the value of type α that is needed in order to unlock -the function f is hidden inside of u is directly analogous to the -concept of "data hiding" in object-oriented programming. See Pierce's -discussion of how to extend system F with existential type -quantification by encoding the existential using continuations. - -So the Kliesli type pretty much determines the bind operation. - -## What continuations are doing - -Ok, we have a continuation monad. We derived it from first -principles, and we have seen that it behaves at least in some respects -as we expect a continuation monad to behave (in that it allows us to -give a good implementation of the task). - ## How continuations can simulate other monads Because the continuation monad allows the result type ρ to be any @@ -434,16 +275,3 @@ is return Nothing. Super cool. - - - -## Delimited versus undelimited continuations - -## Natural language requries delimited continuations - - - - - - -"*the* continuation monad"