Formal definition of Scala continuations

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

Solution

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.