+<!-- λ ◊ ≠ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (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
+
+
+
+
+
+