[[!toc]] ##Introducing Continuations## A continuation is "the rest of the program." Or better: an **delimited continuation** is "the rest of the program, up to a certain boundary." An **undelimited continuation** is "the rest of the program, period." Even if you haven't read specifically about this notion (for example, even if you haven't read Chris and Ken's work on using continuations in natural language semantics), you'll have brushed shoulders with it already several times in this course. A naive semantics for atomic sentences will say the subject term is of type `e`, and the predicate of type `e -> t`, and that the subject provides an argument to the function expressed by the predicate. Monatague proposed we instead take subject terms to be of type `(e -> t) -> t`, and that now it'd be the predicate (still of type `e -> t`) that provides an argument to the function expressed by the subject. If all the subject did then was supply an `e` to the `e -> t` it receives as an argument, we wouldn't have gained anything we weren't already able to do. But of course, there are other things the subject can do with the `e -> t` it receives as an argument. For instance, it can check whether anything in the domain satisfies that `e -> t`; or whether most things do; and so on. This inversion of who is the argument and who is the function receiving the argument is paradigmatic of working with continuations. We did the same thing ourselves back in the early days of the seminar, for example in our implementation of pairs. In the untyped lambda calculus, we identified the pair `(x, y)` with a function: \handler. handler x y A pair-handling function would accept the two elements of a pair as arguments, and then do something with one or both of them. The important point here is that the handler was supplied as an argument to the pair. Eventually, the handler would itself be supplied with arguments. But only after it was supplied as an argument to the pair. This inverts the order you'd expect about what is the data or argument, and what is the function that operates on it. Consider a complex computation, such as: 1 + 2 * (1 - g (3 + 4)) Part of this computation---`3 + 4`---leads up to supplying `g` with an argument. The rest of the computation---`1 + 2 * (1 - ___)`---waits for the result of applying `g` to that argument and will go on to do something with it (inserting the result into the `___` slot). That "rest of the computation" can be regarded as a function: \result. 1 + 2 * (1 - result) This function will be applied to whatever is the result of `g (3 + 4)`. So this function can be called the *continuation* of that application of `g`. For some purposes, it's useful to be able to invert the function/argument order here, and rather than supplying the result of applying `g` to the continuation, we instead supply the continuation to `g`. Well, not to `g` itself, since `g` only wants a single `int` argument. But we might build some `g`-like function which accepts not just an `int` argument like `g` does, but also a continuation argument. Go back and read the material on "Aborting a Search Through a List" in [[Week4]] for an example of doing this. In very general terms, the strategy is to work with functions like this: let g' k (i : int) = ... do stuff ... ... if you want to abort early, supply an argument to k ... ... do more stuff ... ... normal result in let gcon = fun result -> 1 + 2 * (1 - result) in gcon (g' gcon (3 + 4)) It's a convention to use variables like `k` for continuation arguments. If the function `g'` never supplies an argument to its contination argument `k`, but instead just finishes evaluating to a normal result, that normal result will be delivered to `g'`'s continuation `gcon`, just as happens when we don't pass around any explicit continuation variables. The above snippet of OCaml code doesn't really capture what happens when we pass explicit continuation variables. For suppose that inside `g'`, we do supply an argument to `k`. That would go into the `result` parameter in `gcon`. But then what happens once we've finished evaluating the application of `gcon` to that `result`? In the OCaml snippet above, the final value would then bubble up through the context in the body of `g'` where `k` was applied, and eventually out to the final line of the snippet, where it once again supplied an argument to `gcon`. That's not what happens with a real continuation. A real continuation works more like this: let g' k (i : int) = ... do stuff ... ... if you want to abort early, supply an argument to k ... ... do more stuff ... ... normal result in let gcon = fun result -> let final_value = 1 + 2 * (1 - result) in end_program_with final_value in gcon (g' gcon (3 + 4)) So once we've finished evaluating the application of `gcon` to a `result`, the program is finished. (This is how undelimited continuations behave. We'll discuss delimited continuations later.) So now, guess what would be the result of doing the following: let g' k (i : int) = 1 + k i in let gcon = fun result -> let final_value = (1, result) in end_program_with final_value in gcon (g' gcon (3 + 4))