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.
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))
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"
# 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"")
the shift' operator sees as its argument k by replacing ⇧ and ¢ with
their definitions:
+<pre>
⇧+ ¢ ⇧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
~~> shift(\x.⇧c(\x'.(+a)((+x)x'))))
= shift(\x.(\k.kc)(\x'.(+a)((+x)x'))))
~~> shift(\x.(+a)((+x)c))
+</pre>
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
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
Super cool.
-
-
-
-## Delimited versus undelimited continuations
-
-## Natural language requries delimited continuations
-
-
-
-
-
-
-"*the* continuation monad"