- t2 = map2 (++) (mid "a")
- (map2 (++) (mid "b")
- (map2 (++) shift
- (map2 (++) (mid "d")
- (mid []))))
- t2 (\k->k) == "ababdd"
-
-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.
-
-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.
+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:
+
+<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
+ ~~> (\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))
+</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 see how to understand what is going on
+when we talk about quantifier raising in the next lecture.