+Today we're going to encounter continuations. We're going to come at
+them from three different directions, and each time we're going to end
+up at the same place: a particular monad, which we'll call the
+continuation monad.
+
+The three approches are:
+
+* Rethinking the list monad;
+* Montague's PTQ treatment of DPs as generalized quantifiers; and
+* Refunctionalizing zippers (Shan: zippers are defunctionalized continuations);
+
+Rethinking the list monad
+-------------------------
+
+To construct a monad, the key element is to settle on a type
+constructor, and the monad naturally follows from that. I'll remind
+you of some examples of how monads follow from the type constructor in
+a moment. This will involve some review of familair material, but
+it's worth doing for two reasons: it will set up a pattern for the new
+discussion further below, and it will tie together some previously
+unconnected elements of the course (more specifically, version 3 lists
+and monads).
+
+For instance, take the **Reader Monad**. Once we decide that the type
+constructor is
+
+ type 'a reader = fun e:env -> 'a
+
+then we can deduce the unit and the bind:
+
+ runit x:'a -> 'a reader = fun (e:env) -> x
+
+Since the type of an `'a reader` is `fun e:env -> 'a` (by definition),
+the type of the `runit` function is `'a -> e:env -> 'a`, which is a
+specific case of the type of the *K* combinator. So it makes sense
+that *K* is the unit for the reader monad.
+
+Since the type of the `bind` operator is required to be
+
+ r_bind:('a reader) -> ('a -> 'b reader) -> ('b reader)
+
+We can deduce the correct `bind` function as follows:
+
+ r_bind (u:'a reader) (f:'a -> 'b reader):('b reader) =
+
+We have to open up the `u` box and get out the `'a` object in order to
+feed it to `f`. Since `u` is a function from environments to
+objects of type `'a`, we'll have
+
+ .... f (u e) ...
+
+This subexpression types to `'b reader`, which is good. The only
+problem is that we don't have an `e`, so we have to abstract over that
+variable:
+
+ fun e -> f (u e) ...
+
+This types to `env -> 'b reader`, but we want to end up with `env ->
+'b`. The easiest way to turn a 'b reader into a 'b is to apply it to
+an environment. So we end up as follows:
+
+ r_bind (u:'a reader) (f:'a -> 'b reader):('b reader) = f (u e) e
+
+And we're done.
+
+The **State Monad** is similar. We somehow intuit that we want to use
+the following type constructor:
+
+ type 'a state = 'store -> ('a, 'store)
+
+So our unit is naturally
+
+ let s_unit (x:'a):('a state) = fun (s:'store) -> (x, s)
+
+And we deduce the bind in a way similar to the reasoning given above.
+First, we need to apply `f` to the contents of the `u` box:
+
+ let s_bind (u:'a state) (f:'a -> ('b state)):('b state) =
+
+But unlocking the `u` box is a little more complicated. As before, we
+need to posit a state `s` that we can apply `u` to. Once we do so,
+however, we won't have an `'a`, we'll have a pair whose first element
+is an `'a`. So we have to unpack the pair:
+
+ ... let (a, s') = u s in ... (f a) ...
+
+Abstracting over the `s` and adjusting the types gives the result:
+
+ let s_bind (u:'a state) (f:'a -> ('b state)):('b state) =
+ fun (s:state) -> let (a, s') = u s in f a s'
+
+The **Option Monad** doesn't follow the same pattern so closely, so we
+won't pause to explore it here, though conceptually its unit and bind
+follow just as naturally from its type constructor.
+
+Our other familiar monad is the **List Monad**, which we were told
+looks like this:
+
+ type 'a list = ['a];;
+ l_unit (x:'a) = [x];;
+ l_bind u f = List.concat (List.map f u);;
+
+Recall that `List.map` take a function and a list and returns the
+result to applying the function to the elements of the list:
+
+ List.map (fun i -> [i;i+1]) [1;2] ~~> [[1; 2]; [2; 3]]
+
+and List.concat takes a list of lists and erases the embdded list
+boundaries:
+
+ List.concat [[1; 2]; [2; 3]] ~~> [1; 2; 2; 3]
+
+And sure enough,
+
+ l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3]
+
+But where is the reasoning that led us to this unit and bind?
+And what is the type `['a]`? Magic.
+
+So let's take a *completely useless digressing* and see if we can
+gain some insight into the details of the List monad. Let's choose
+type constructor that we can peer into, using some of the technology
+we built up so laboriously during the first half of the course. I'm
+going to use type 3 lists, partly because I know they'll give the
+result I want, but also because they're my favorite. These were the
+lists that made lists look like Church numerals with extra bits
+embdded in them:
+
+ empty list: fun f z -> z
+ list with one element: fun f z -> f 1 z
+ list with two elements: fun f z -> f 2 (f 1 z)
+ list with three elements: fun f z -> f 3 (f 2 (f 1 z))
+
+and so on. To save time, we'll let the Ocaml interpreter infer the
+principle types of these functions (rather than deducing what the
+types should be):
+
+<pre>
+# fun f z -> z;;
+- : 'a -> 'b -> 'b = <fun>
+# fun f z -> f 1 z;;
+- : (int -> 'a -> 'b) -> 'a -> 'b = <fun>
+# fun f z -> f 2 (f 1 z);;
+- : (int -> 'a -> 'a) -> 'a -> 'a = <fun>
+# fun f z -> f 3 (f 2 (f 1 z))
+- : (int -> 'a -> 'a) -> 'a -> 'a = <fun>
+</pre>
+
+Finally, we're getting consistent principle types, so we can stop.
+These types should remind you of the simply-typed lambda calculus
+types for Church numerals (`(o -> o) -> o -> o`) with one extra bit
+thrown in (in this case, and int).
+
+So here's our type constructor for our hand-rolled lists:
+
+ type 'a list' = (int -> 'a -> 'a) -> 'a -> 'a
+
+Generalizing to lists that contain any kind of element (not just
+ints), we have
+
+ type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
+
+So an `('a, 'b) list'` is a list containing elements of type `'a`,
+where `'b` is the type of some part of the plumbing. This is more
+general than an ordinary Ocaml list, but we'll see how to map them
+into Ocaml lists soon. We don't need to grasp the role of the `'b`'s
+in order to proceed to build a monad:
+
+ l'_unit (x:'a):(('a, 'b) list) = fun x -> fun f z -> f x z
+
+No problem. Arriving at bind is a little more complicated, but
+exactly the same principles apply, you just have to be careful and
+systematic about it.
+
+ l'_bind (u:('a,'b) list') (f:'a -> ('c, 'd) list'): ('c, 'd) list' = ...
+
+Unfortunately, we'll need to spell out the types:
+
+ l'_bind (u: ('a -> 'b -> 'b) -> 'b -> 'b)
+ (f: 'a -> ('c -> 'd -> 'd) -> 'd -> 'd)
+ : ('c -> 'd -> 'd) -> 'd -> 'd = ...
+
+It's a rookie mistake to quail before complicated types. You should
+be no more intimiated by complex types than by a linguistic tree with
+deeply embedded branches: complex structure created by repeated
+application of simple rules.
+
+As usual, we need to unpack the `u` box. Examine the type of `u`.
+This time, `u` will only deliver up its contents if we give `u` as an
+argument a function expecting an `'a`. Once that argument is applied
+to an object of type `'a`, we'll have what we need. Thus:
+
+ .... u (fun (x:'a) -> ... (f a) ... ) ...
+
+In order for `u` to have the kind of argument it needs, we have to
+adjust `(f a)` (which has type `('c -> 'd -> 'd) -> 'd -> 'd`) in
+order to deliver something of type `'b -> 'b`. The easiest way is to
+alias `'d` to `'b`, and provide `(f a)` with an argument of type `'c
+-> 'b -> 'b`. Thus:
+
+ l'_bind (u: ('a -> 'b -> 'b) -> 'b -> 'b)
+ (f: 'a -> ('c -> 'b -> 'b) -> 'b -> 'b)
+ : ('c -> 'b -> 'b) -> 'b -> 'b =
+ .... u (fun (x:'a) -> f a k) ...
+
+[Excercise: can you arrive at a fully general bind for this type
+constructor, one that does not collapse `'d`'s with `'b`'s?]
+
+As usual, we have to abstract over `k`, but this time, no further
+adjustments are needed:
+
+ l'_bind (u: ('a -> 'b -> 'b) -> 'b -> 'b)
+ (f: 'a -> ('c -> 'b -> 'b) -> 'b -> 'b)
+ : ('c -> 'b -> 'b) -> 'b -> 'b =
+ fun (k:'c -> 'b -> 'b) -> u (fun (x:'a) -> f a k)
+
+You should carefully check to make sure that this term is consistent
+with the typing.
+
+Our theory is that this monad should be capable of exactly
+replicating the behavior of the standard List monad. Let's test:
+
+
+ l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3]
+
+ l'_bind (fun f z -> f 1 (f 2 z))
+ (fun i -> fun f z -> f i (f (i+1) z)) ~~> <fun>
+
+Sigh. Ocaml won't show us our own list. So we have to choose an `f`
+and a `z` that will turn our hand-crafted lists into standard Ocaml
+lists, so that they will print out.
+
+# let cons h t = h :: t;; (* Ocaml is stupid about :: *)
+# l'_bind (fun f z -> f 1 (f 2 z))
+ (fun i -> fun f z -> f i (f (i+1) z)) cons [];;
+- : int list = [1; 2; 2; 3]
+
+Ta da!
+
+Just for mnemonic purposes (sneaking in an instance of eta reduction
+to the definition of unit), we can summarize the result as follows:
+
+ type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
+ l'_unit x = fun f -> f x
+ l'_bind u f = fun k -> u (fun x -> f x k)
+
+To bad this digression, though it ties together various
+elements of the course, has *no relevance whatsoever* to the topic of
+continuations.
+