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.

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({...}).

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?