X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week14_continuations.mdwn;h=ba2475f24b55ce0b9310180476b6715dca7aba6b;hp=0000000000000000000000000000000000000000;hb=8a9edd44b9db8300cfc2acc269bb11562911951c;hpb=7f466e5d1959494164e54354a08abc88eeb1b3ad;ds=sidebyside

diff --git a/topics/_week14_continuations.mdwn b/topics/_week14_continuations.mdwn
new file mode 100644
index 00000000..ba2475f2
--- /dev/null
+++ b/topics/_week14_continuations.mdwn
@@ -0,0 +1,188 @@
+<!-- λ ◊ ≠ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
+
+[[!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
+followin fashion.
+
+## The continuation monad
+
+Let's take a look at some of our favorite monads from the point of
+view of types.  Here, `==>` is the Kleisli arrow.
+
+    Reader monad: types: Mα ==> β -> α
+                  ⇧: \ae.a : α -> Mα
+                  compose: \fghe.f(ghe)e : (Q->MR)->(P->MQ)->(P->MR)
+                  gloss: copy environment and distribute it to f and g
+
+    State monad: types: α ==> β -> (α x β)
+                 ⇧: \ae.(a,e) : α -> Mα
+                 compose: \fghe.let (x,s) = ghe in fxs
+                 thread the state through g, then through f                 
+
+    List monad: types: α ==> [α]
+                ⇧: \a.[a] : α -> Mα
+                compose: \fgh.concat(map f (gh))
+                gloss: compose f and g pointwise
+
+    Maybe monad: types: α ==> Nothing | Just α
+                ⇧: \a. Just a
+                compose: \fgh.
+		  case gh of Nothing -> Nothing
+		           | Just x -> case fx of Nothing -> Nothing
+                                                | Just y -> Just y
+                gloss: strong Kline
+
+Now we need a type for a continuation.  A continuized term is one that
+expects its continuation as an argument.  The continuation of a term
+is a function from the normal value of that term to a result.  So if
+the term has type continuized term has type α, the continuized version
+has type (α -> ρ) -> ρ:
+
+    Continuation monad: types: Mα => (α -> ρ) -> ρ
+                        ⇧: \ak.ka
+                        compose: \fghk.f(\f'.g h (\g'.f(g'h)
+			gloss: first give the continuation to f, then build
+                               a continuation out of the result to give to 
+
+The first thing we should do is demonstrate that this monad is
+suitable for accomplishing the task.
+
+We lift the computation `("a" ++ ("b" ++ ("c" ++ "d")))` into 
+the monad as follows:
+
+    t1 = (map1 ((++) "a") (map1 ((++) "b") (map1 ((++) "c") (mid "d"))))
+
+Here, `(++) "a"` is a function of type [Char] -> [Char] that prepends
+the string "a", so `map1 ((++) "a")` takes a string continuation k and
+returns a new string continuation that takes a string s returns "a" ++ k(s).
+So `t1 (\k->k) == "abcd"`.
+
+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 (String -> String) -> String,
+and a string continuation k of type String -> String.  Since u is the
+result returned by 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.
+
+Note that the shift operator constructs a new continuation by
+composing its second argument with itself (i.e., the new doubled
+continuation is \s.k(ks)).  Once it has constructed this
+new continuation, it delivers it as an argument to the remaining part
+of the computation!  
+
+    (map1 ((++) "a") (map1 ((++) "b") (shift (mid "d")))) (\k->k) == "ababd"
+
+Let's just make sure that we have the left-to-right evaluation we were
+hoping for by evaluating "abSdeSf":
+
+    t6 = map1 ((++) "a")
+              (map1 ((++) "b")
+                    (shift
+		      (map1 ((++) "d")
+                            (map1 ((++) "e")
+                                  (shift (mid "f"))))))
+
+    t6 (\k->k) == "ababdeababdef"
+
+As expected.
+
+In order to add a reset operator #, we can have
+
+    # u k = k(u(\k.k))
+    ab#deSf ~~> abdedef
+
+Note that the lifting of the original unmonadized computation treated
+prepending "a" as a one-place operation.  If we decompose this
+operation into a two-place operation of appending combined with a
+string "a", an interesting thing happens.
+
+
+    map2 f u v k = u(\u' -> v (\v' -> k(f u' v'))) 
+    shift k = k (k "")
+
+    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?
+
+This depends on which S is executed first.  Assume the first 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 parenthesese are added to
+show stages in the construction of the final result).
+
+Note that this is a different result than assuming that what execution
+does is choose an S, and double its context, 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 (on the bi-directional continuation
+perspective).
+
+
+## Viewing Montague's PTQ as CPS
+
+
+
+
+
+## How continuations can simulate other monads
+
+## Delimited versus undelimited continuations
+
+## Natural language requries delimited continuations
+
+
+
+
+
+