No entiendo el tipeo de las continuaciones delimitadas de Scala (A @cpsParam [B, C])

Question

Tengo dificultades para entender qué significa exactamente cuando un valor tiene el tipo A @cpsParam[B,C] y qué tipos de esta forma debo asignar a mis valores cuando uso la facilidad de continuación delimitada.

He mirado en algunas fuentes:

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

pero no me dio mucha intuición en esto. En el último enlace, el autor intenta dar una explicación explícita, pero de todos modos no está lo suficientemente claro.

El A aquí representa el resultado del cálculo, que también es la entrada a su continuación. B representa el tipo de devolución de esa continuación, y C representa su tipo de devolución "final", porque shift puede hacer un procesamiento posterior del valor devuelto y cambiar su tipo.

No entiendo la diferencia entre "salida del cálculo", "tipo de devolución de la continuación" y "tipo de devolución final de la continuación". Suenan como sinónimos.

Answer 1

Entonces, la gente me ayudó con esto en otro lado. Aquí está la respuesta:

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

Así, shift es un agujero de tipo A, dentro del cálculo del tipo {...}B. El argumento de shift devuelve un valor de tipo C y es por eso que reset ({...}) tiene el tipo C.

El truco clave para entender esto fue ver que {...} y tienen un tipo diferente según el tipo que devuelva el argumento shift.

Por ejemplo:

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

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

Aquí A es Int, B es String, C es List[String] porque es {"number" + _} (aquí) una función a partir Int a String y el argumento de shift, dado que la función, produce una List[String], que se convierte en el resultado de reset({...}).

Answer 2

Todavía estoy en el proceso de descifrar las reglas/implicaciones de tipeo exactas involucradas aquí.

Parece fácil/fácil si los tipos en los ejemplos son "lo suficientemente simples" para "encajar bien" como se muestra arriba, pero se vuelve más interesante/difícil (al menos para mí) al comparar cosas con el mecanografiado por tiark rompf:

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

por lo que el resultado de [|e|].map((x: A) => {[|r|]}) tendrá el tipo Shift[U,B,C] acuerdo con la definición del mapa dado en el documento de tiark.

Aquí U no es necesariamente el mismo que B.

Hasta ahora no entiendo por qué U se le permite ser diferente de B sin algo así como U <: B dada en la definición de un mapa en el documento de tiark.

¿Qué me falta por defecto al no entender aquí?

¿Algún consejo/idea?