X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week14_continuations.mdwn;h=0000000000000000000000000000000000000000;hp=42f2c1180d924d655c74f3ff1b3936e0d569ac51;hb=30e80630a4bdb0ec23dd7098f735b060f6a3de0f;hpb=1efbaa05ade48388ad996f60091c9b6f8bc58c1d diff --git a/topics/_week14_continuations.mdwn b/topics/_week14_continuations.mdwn deleted file mode 100644 index 42f2c118..00000000 --- a/topics/_week14_continuations.mdwn +++ /dev/null @@ -1,277 +0,0 @@ - - -[[!toc]] - -# Continuations - -Last week we saw how to turn a list zipper into a continuation-based -list processor. The function computed something we called "the task", -which was a simplified langauge involving control operators. - - abSdS ~~> ababdS ~~> ababdababd - -The task is to process the list from left to right, and at each "S", -double the list so far. Here, "S" is a kind of control operator, and -captures the entire previous computation. We also considered a -variant in which '#' delimited the portion of the list to be copied: - - ab#deSfg ~~> abededfg - -In this variant, "S" and "#" correspond to `shift` and `reset`, which -provide access to delimited continuations. - -The expository logic of starting with this simplified task is the -notion that as lists are to trees, so is this task to full-blown -continuations. So to the extent that, say, list zippers are easier to -grasp than tree zippers, the task is easier to grasp than full -continuations. - -We then presented CPS transforms, and demonstrated how they provide -an order-independent analysis of order of evaluation. - -In order to continue to explore continuations, we will proceed in the -following fashion: we introduce the traditional continuation monad, -and show how it solves the task, then generalize the task to -include doubling of both the left and the right context. - -## The continuation monad - -In order to build a monad, we start with a Kleisli arrow. - - Continuation monad: types: given some ρ, Mα => (α -> ρ) -> ρ - ⇧ == \ak.ka : a -> Ma - bind == \ufk. u(\x.fxk) - -We'll first show that this monad solves the task, then we'll consider -the monad in more detail. - -The unmonadized computation (without the shifty "S" operator) is - - t1 = + a (+ b (+ c d)) ~~> abcd - -where "+" is string concatenation and the symbol a is shorthand for -the string "a". - -In order to use the continuation monad to solve the list task, -we choose α = ρ = [Char]. So "abcd" is a list of characters, and -a boxed list has type M[Char] == ([Char] -> [Char]) -> [Char]. - -Writing ¢ in between its arguments, t1 corresponds to the following -monadic computation: - - mt1 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ ⇧c ¢ ⇧d)) - -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 - - ¢ M N = \k -> M (\f -> N (\a -> k(f x))) - -for the continuation monad. - -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 - -That is, the original computation is the monadic version applied to -the trivial continuation. - -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)) - -We can now define a shift operator to perform the work of "S": - - shift u k = u(\s.k(ks)) - -Shift takes two arguments: a string continuation u of type M[Char], -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. The expression `\s.k(ks)` is just the composition of k with itself. - - mt2 I == "ababd" - -just as desired. - -Let's just make sure that we have the left-to-right evaluation we were -hoping for by evaluating "abSdeSf": - - mt3 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ (⇧+ ¢ ⇧d ¢ (⇧+ ¢ ⇧e ¢ (shift ⇧f))))) - -Then - - mt3 I = "ababdeababdef" -- structure: (ababde)(ababde)f - - -As expected. - -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 (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"") - -This shift operator takes a continuation k of type [Char]->[Char], and -invokes it twice. Since k requires an argument of type [Char], we -need to use the first invocation of k to construction a [Char]; we do -this by feeding it a string. Since the task does not replace the -shift operator with any marker, we give the empty string "" as the -argument. - -But now the new shift operator captures more than just the preceeding -part of the construction---it captures the entire context, including -the portion of the sequence that follows it. That is, - - mt4 I = "ababdd" - -We have replaced "S" in "abSd" with "ab_d", where the underbar will be -replaced with the empty string supplied in the definition of shift'. -Crucially, not only is the prefix "ab" duplicated, so is the suffix -"d". - -Things get interesting when we have more than one operator in the -initial list. What should we expect if we start with "aScSe"? -If we assume that when we evaluate each S, all the other S's become -temporarily inert, we expect a reduction path like - - aScSe ~~> aacSecSe - -But note that the output has just as many S's as the input--if that is -what our reduction strategy delivers, then any initial string with -more than one S will never reach a normal form. - -But that's not what the continuation operator shift' delivers. - - mt5 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ shift' ¢ (⇧+ ¢ ⇧c ¢ (⇧+ ¢ shift' ¢ "e"))) - - mt5 I = "aacaceecaacaceecee" -- structure: "aacaceecaacaceecee" - -Huh? - -This is considerably harder to understand than the original list task. -The key is figuring out in each case what function the argument k to -the shift operator gets bound to. - -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
-   ~~> (\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(\x.I(fx))) 
-   ~~> (\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(f)) 
-   ~~> ⇧+(\f.⇧a(\x.(\f.(⇧+ ¢ shift' ¢ ⇧c)(f))(fx)))) 
-   ~~> ⇧+(\f.⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(fx)))
-   = (\k.k+)(\f.⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(fx)))
-   ~~> ⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(+x))
-   = (\k.ka)(\x.(⇧+ ¢ shift' ¢ ⇧c)(+x))
-   ~~> (⇧+ ¢ shift' ¢ ⇧c)(+a)
-   = (\k.⇧+(\f.shift(\x.k(fx)))) ¢ ⇧c (+a)
-   = (\k.(\k.⇧+(\f.shift(\x.k(fx))))(\f.⇧c(\x.k(fx))))(+a)
-   ~~> (\k.⇧+(\f.shift(\x.k(fx))))(\f'.⇧c(\x'.(+a)(f'x')))
-   ~~> ⇧+(\f.shift(\x.(\f'.⇧c(\x'.(+a)(f'x')))(fx)))
-   ~~> ⇧+(\f.shift(\x.⇧c(\x'.(+a)((fx)x'))))
-   = (\k.k+)(\f.shift(\x.⇧c(\x'.(+a)((fx)x'))))
-   ~~> 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 see how to understand what is going on -when we talk about quantifier raising in the next lecture. - -## Viewing Montague's PTQ as CPS - -Montague's conception of determiner phrases as generalized quantifiers -is a limited form of continuation-passing. (See, e.g., chapter 4 of -Barker and Shan 2014.) Start by assuming that ordinary DPs such as -proper names denote objects of type `e`. Then verb phrases denote -functions from individuals to truth values, i.e., functions of type `e --> t`. - -The meaning of extraordinary DPs such as *every woman* or *no dog* -can't be expressed as a simple individual. As Montague argued, it -works much better to view them as predicates on verb phrase meanings, -i.e., as having type `(e->t)->t`. Then *no woman left* is true just -in case the property of leaving is true of no woman: - - no woman: \k.not \exists x . (woman x) & kx - left: \x.left x - (no woman) (left) = not \exists x . woman x & left x - -Montague also proposed that all determiner phrases should have the -same type. After all, we can coordinate proper names with -quantificational DPs, as in *John and no dog left*. Then generalized -quantifier corresponding to the proper name *John* is the quantifier -`\k.kj`. - -## How continuations can simulate other monads - -Because the continuation monad allows the result type ρ to be any -type, we can choose ρ in clever ways that allow us to simulate other -monads. - - Reader: ρ = env -> α - State: ρ = s -> (α, s) - Maybe: ρ = Just α | Nothing - -You see how this is going to go. Let's see an example by adding an -abort operator to our task language, which represents what -we want to have happen if we divide by zero, where what we want to do -is return Nothing. - - abort k = Nothing - mid a k = k a - map2 f u v k = u(\u' -> v (\v' -> k(f u' v'))) - t13 = map2 (++) (mid "a") - (map2 (++) (mid "b") - (map2 (++) (mid "c") - (mid "d"))) - - t13 (\k->Just k) == Just "abcd" - - t14 = map2 (++) (mid "a") - (map2 (++) abort - (map2 (++) (mid "c") - (mid "d"))) - - - t14 (\k->Just k) == Nothing - -Super cool. -