No entiendo la tipificación de las continuaciones delimitadas de Scala (A @cpsParam [B, C])

Question

Estoy tratando de entender lo que precisamente significa cuando un valor es de tipo A @cpsParam[B,C] y qué tipos de esta forma debería asignar a mis valores al utilizar la instalación continuaciones delimitado.

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 dieron mucha intuición en esto. En el último eslabón, el autor trata de dar una explicación explícita, pero no es lo suficientemente clara de todos modos.

  

El A aquí representa la salida de la computación, que es también la entrada a su continuación. El B representa el tipo de retorno de que la continuación, y la C representa su tipo, porque "final" de retorno de cambio puede hacer procesamiento adicional para el valor devuelto y cambiar su tipo.

No entiendo la diferencia entre "la salida de la computación", "tipo de retorno de la continuación" y "tipo de retorno definitivo de la continuación". Suenan como sinónimos.

Answer 1

Por lo tanto, la gente me ayudó con éste en otro lugar. Aquí está la respuesta:

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

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

El truco clave en la comprensión de estas cosas fue ver que {...} y reset {...} tienen diferentes tipos dependiendo de qué tipo de argumentos rendimientos del shift.

Por ejemplo:

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

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

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

Answer 2

Todavía estoy en un proceso de averiguar la tipificación exactas reglas / consecuencias implicadas en aquí.

Parece fácil / más fácil si los tipos en los ejemplos son "bastante simple" a "encajar bien" como se muestra arriba, pero se vuelve más sin interés / difícil (al menos para mí) en la comparación de las cosas a la tipificación dar 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 parecido U <: B dada en la definición de un mapa en el documento de tiark.

¿Qué me falta repsectively no entender aquí?

Cualquier consejos / ideas?