Formal definition of Scala continuations

Question

There are some questions about what Scala continuations are (here and here). But the answers only try to explain it. So in this question I'm asking for a formal definition of what (Scala's) delimited continuations are. I don't require an example (though it might help) and ask for a simple and understandable as possible formalization, maybe even ignoring typing if it helps.

The formalization should cover syntax (not in the grammatical sense but rather like f is a function and c is a foo) and semantics (what will be the result of the computation).

Answer 1

Scala delimited continuations as implemented in the continuation plugin are an adaptation of the shift and reset control operators introduced by Danvy and Filinski. See their Abstracting Control and Representing Control: A Study of the CPS Transformation papers from 1990 and 1992. In the context of typed language, the work from the EPFL team extends the work of Asai. See the 2007 papers here.

That should be plenty of formalism! I glanced at those and unfortunately they require fluency in lambda calculus notation.

On the other hand, I found the following Programming with Shift and Reset tutorial and it feels like I really had a breakthrough in understanding when I started to translate the examples to Scala and when I got to section "2.6 How to extract delimited continuations".

The reset operator delimits a piece of the program. shift is used in a location where a value is present (including possibly Unit). You can think of it as a hole. Let's represent it with ◉.

So let's look at the following expressions:

reset { 3 + ◉ - 1 }                  // (1)
reset {                              // (2)
  val s = if (◉) "hello" else "hi"
  s + " world"
}
reset {                              // (3)
  val s = "x" + (◉: Int).toString
  s.length
}

What shift does is to turn the program inside the reset into a function that you can access (this process is called reification). In the cases above, the functions are:

val f1 = (i: Int) => 3 + i - 1       // (1)
val f2 = (b: Boolean) => {
   val s = if (b) "hello" else "hi"  // (2)
   s + " world"
}
val f3 = (i: Int) => {               // (3)
   val s = "x" + i.toString
   s.length
}

The function is called the continuation and is provided as an argument to its own argument. shift signature is:

shift[A, B, C](fun: ((A) => B) => C): A 

The continuation will be the (A => B) function and whoever writes the code inside the shift decides what to do (or not to do) with it. You really get a feeling for what it can do if you simply return it. The result of the reset is then that reified computation itself:

val f1 = reset { 3 + shift{ (k:Int=>Int) => k } - 1 }
val f2 = reset { 
           val s =
             if (shift{(k:Boolean=>String) => k}) "hello"
             else "hi"
           s + " world"
         }
val f3 = reset {
           val s = "x" + (shift{ (k:Int=>Int) => k}).toString
           s.length
         }

I think the reification aspect is really an important aspect of understanding the Scala delimited continuations.

From a type perspective, if the function k has type (A=>B) then the shift has type A@cpsParam[B,C]. The type C is purely determined by what you chose to return inside the shift. A expression returning a type annotated with cpsParam or cps is qualified as impure in the EPFL paper. This is as opposed to a pure expression, that does not have cps-annotated types.

Impure computations are transformed into Shift[A, B, C] objects (now called ControlContext[A, B, C] in the standard library). The Shift objects are extending the continuation monad. Their formal implementation is in the EPFL paper, section 3.1 page 4. The map method combines a pure computation with the Shift object. The flatMap method combines an impure computation with the Shift object.

The continuation plugin performs the code transformation following the outline given in section 3.4 of the EPLF paper. Basically, shift are turned into Shift objects. Pure expressions that occurs after are combined with maps, impure ones are combined with flatMaps (see more rules figure 4). Finally once all has been converted up to the enclosing reset, if everything type-checks, the type of the final Shift object after all the maps and flatMaps should be Shift[A, A, C]. The reset function reifies the contained Shift and calls the function with the identity function as argument.

In conclusion, I think the EPLF paper does contain a formal description of what happens (sections 3.1 and 3.4 and figure 4). The tutorial that I mention has very well chosen examples that give a great feel for delimited continuations.

Answer 2

To quote the wikipedia:

a delimited continuation, composable continuation or partial continuation, is a "slice" of a continuation frame that has been reified into a function.

Scala syntax for this is:

// Assuming g: X => anything
reset {
  A
  g(shift { (f: (X) => Y) => /* code using function f */ })
  B
}

A continuation frame above is everything that would be executed after the shift up until the end of the block delimited by reset. That includes calling the function g, since it would only be called after evaluating shift, plus all the code in B.

The function g is not required -- one could be calling a method instead, or completely ignore the result of shift. I show it just to make clear that the shift call returns a value that can be used.

In other words, that continuation frame becomes the following function:

// Assuming g: X => anything
def f: (X) => Y = { x => 
    g(x)
    B
}

And the whole reset body becomes this:

// Assuming g: X => anything
A
def f: (X) => Y = { x => 
    g(x)
    B
}
/* code using function f */

Note that the last statement in B must have type Y. The result of the computation is the result of the contents of the shift block, as would happen with that translation above.

If you want more precision, check the paper that describes delimited continuations in Scala. The exact types can be found on the API documentation.