author Chris Thu, 7 May 2015 15:32:55 +0000 (11:32 -0400) committer Chris Thu, 7 May 2015 15:32:55 +0000 (11:32 -0400)

index ba2475f..bb68260 100644 (file)
@@ -148,34 +148,170 @@ 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
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,
+`(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
continuations allow functions to see into the future!

What do you expect will be the result of executing "aScSe" under the
-second perspective?
+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.

-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).
+## Viewing Montague's PTQ as CPS

-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).
+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`.
+
+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

-## Viewing Montague's PTQ as CPS
+Because the continuation monad allows the result type ρ to be any
+type, we can choose ρ in clever ways that allow us to simulate other

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

-## How continuations can simulate other monads

## Delimited versus undelimited continuations

## Delimited versus undelimited continuations