[lambda.git] / topics / _week14_continuations.mdwn

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

<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.

## 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.