Don't understand the typing of Scala's delimited continuations (A @cpsParam[B,C])

Question

I'm struggling to understand what precisely does it mean when a value has type A @cpsParam[B,C] and what types of this form should I assign to my values when using the delimited continuations facility.

I've looked at some sources:

http://lamp.epfl.ch/~rompf/continuations-icfp09.pdf

http://www.scala-lang.org/node/2096

http://dcsobral.blogspot.com/2009/07/delimited-continuations-explained-in.html

http://blog.richdougherty.com/2009/02/delimited-continuations-in-scala_24.html

but they didn't give me much intuition into this. In the last link, the author tries to give an explicit explanation, but it is not clear enough anyway.

The A here represents the output of the computation, which is also the input to its continuation. The B represents the return type of that continuation, and the C represents its "final" return type—because shift can do further processing to the returned value and change its type.

I don't understand the difference between "output of the computation", "return type of the continuation" and "final return type of the continuation". They sound like synonyms.

Longoria

I'm always sad when folks don't get to see my blog post: suereth.blogspot.com/2010/03/… I cover this in detail, as it was something that frustrated me greatly looking at existing sources on the internet. – Geophysics

Thanks Josh, I shall look at your post. – Longoria

Answer 1

So, people helped me with this one elsewhere. Here is the answer:

reset ({
    ...
    ...shift((k:A=>B) => ...::C)::A...
    ...
}::B)::C

So, shift is a hole of type A in a computation {...} of type B. The argument of shift returns a value of type C and that's why reset ({...}) has type C.

The key trick in understanding this stuff was to see that {...} and reset {...} have different type depending on what type the shift's argument returns.

For example:

reset ({
    "number "+shift((k:Int=>String) => List(k(1), k(2), k(3)))
})

returns List("number 1", "number 2", "number 3").

Here A is Int, B is String, C is List[String] because {"number" + _} is (here) a function from Int to String and the argument of shift, given that function, produces a List[String], which becomes result of the reset({...}).

Longoria

Answer 2

I am still in a process of figuring out the exact typing rules/implications involved in here.

It seems easy/easier if the types in the examples are "simple enough" to "fit well" as shown above, but it becomes more interresting/difficult (at least for me) in comparing things to the typing give by tiark rompf:

|- e: A@cpsParam[B,C]; {[|r|]}: U
-----------------------------------------------------
[|val x: A = e; r|] = [|e|].map( (x: A) => {[|r|]} )

so the result of [|e|].map( (x: A) => {[|r|]} ) will have the type Shift[U,B,C] according to the definition of map given in tiark's paper.

Here U is not necessarily be the same as B.

So far I do not understand why U is allowed to be different from B without something like U <: B given in the definition of map in tiark's paper.

What am I missing repsectively failing to understand here?

Any tips/ideas?

Ineducation