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.

Answer 3

Continuations allow you to can capture the code after your shift (but inside your reset) and apply it like so:

  import scala.util.continuations._
  def main(args: Array[String]): Unit = {
    reset {
      shift { continue: (Int => Int) =>
        val result: Int = continue(continue(continue(7)))
        println("result: " + result) // result: 10
      } + 1
    }
  }

In this case the code outside of our shift (but inside our reset) is +1, so each time you call continue, { _+1 } is applied. Thus the result of continue(continue(continue(7))) is 7 + 1 + 1 + 1, or 10.

Here is some more sample code taken from here:

  import scala.util.continuations._
  import java.util.{Timer,TimerTask}

  def main(args: Array[String]): Unit = {
    val timer = new Timer()
    type ContinuationInputType = Unit
    def sleep(delay: Int) = shift { continue: (ContinuationInputType => Unit) =>
      timer.schedule(new TimerTask {
        val nothing: ContinuationInputType = ()
        def run() = continue(nothing) // in a real program, we'd execute our continuation on a thread pool
      }, delay)
    }
    reset {
      println("look, Ma ...")
      sleep(1000)
      println(" no threads!")
    }
  }

In the above code, the code that is after the shift but inside the reset is println(" no threads!"). Thus if we replace this:

def run() = continue(nothing)

with this:

def run() = continue(continue(continue(nothing)))

We get this output:

look, Ma ...
 no threads!
 no threads!
 no threads!

instead of this output:

look, Ma ...
 no threads!

So our code after this change is basically equivalent to:

  import java.util.{Timer,TimerTask}
  def main(args: Array[String]): Unit = {
    println("look, Ma ...")
    timer.schedule(new TimerTask {
      def run() = {
        println(" no threads!")
        println(" no threads!")
        println(" no threads!")
      }
    }, 1000)
  }

You can play around with the code here.

Note that all the code before our call to continue is only executed once, and all the code between the end of our shift and the end of our reset is executed as many times as continue is called. If our continuation is never called, then the code in between the end of our shift and the end of our reset is never executed. Thus a continuation in Scala is a lambda that captures all the code between the end of a shift and the end of that shift's enclosing reset.

Also note that if our continuation is executed on a thread pool, the rest of the code (all the code between the end of shift and the end of the reset) is executed on the thread given to us by that thread pool. So if our continuation runs on thread pool thread #1, println(" no threads!") will run on thread pool thread #1, but println("look, Ma ...") will run on the main thread. Because of this, the continuation feature can be used to implement a facade on top of asynchronus I/O to make it look like blocking IO.