Definición formal de continuación de Scala

Question

Hay algunas preguntas sobre qué continuación de Scala son (here y here). Pero las respuestas solo intentan explicarlo. Entonces, en esta pregunta, estoy pidiendo una definición formal de las continuaciones delimitadas (de Scala). No necesito un ejemplo (aunque podría ser útil) y solicito una formalización simple y comprensible, incluso ignorando el tipeo si me sirve.

La formalización debe abarcar la sintaxis (no en el sentido gramatical, sino más bien como f is a function and c is a foo) y la semántica (cuál será el resultado del cálculo).

Answer 1

Scala delimitada continuaciones tal como se aplica en el plugin de continuación son una adaptación de la cambio y restablecer operadores de control introducidas por Danvy y Filinski. Ver su Haciendo abstracción de control y de control que representa: Un estudio de la transformación de CPSpapers entre 1990 y 1992. En el contexto de la lengua escrita a máquina, el trabajo del equipo de la EPFL se extiende el trabajo de Asai. Consulte los documentos de 2007 here.

¡Eso debería ser un montón de formalismo! Eché un vistazo a esos y, lamentablemente, requieren fluidez en la notación de cálculo lambda.

Por otro lado, he encontrado el Programación siguiente con Shift y RESETtutorial y se siente como que realmente tenía un gran avance en la comprensión cuando empecé a traducir los ejemplos a Scala y cuando llegué a la sección "2.6 Cómo extraer las continuaciones delimitadas ".

El operador reset delimita una parte del programa. shift se usa en una ubicación donde hay un valor presente (incluida posiblemente la Unidad). Puedes pensar que es un agujero. Vamos a representarlo con ◉.

Así que echemos un vistazo a las siguientes expresiones:

reset { 3 + ◉ - 1 }     // (1) 
reset {        // (2) 
    val s = if (◉) "hello" else "hi" 
    s + " world" 
} 
reset {        // (3) 
    val s = "x" + (◉: Int).toString 
    s.length 
} 

Lo shift hace es convertir el programa en el reinicio en una función que se puede acceder (este proceso se llama la cosificación). En los casos anteriores, las funciones son:

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 
} 

La función se llama la continuación y se proporciona como un argumento para su propio argumento. la firma de desplazamiento es:

shift[A, B, C](fun: ((A) => B) => C): A 

La continuación será el (=> A B) la función y el que escribe el código dentro del shift decide qué hacer (o no hacer) con ella. Realmente tienes una idea de lo que puede hacer si simplemente lo devuelves. El resultado de la reset es entonces que cosifica cómputo en sí:

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 
     } 

Creo que el aspecto reificación es realmente un aspecto importante de la comprensión de la Scala delimitado continuaciones.

Desde una perspectiva de tipo, si la función k tiene el tipo (A => B) entonces el shift tiene el tipo A@cpsParam[B,C]. El tipo C está completamente determinado por lo que elija devolver dentro del shift. Una expresión que devuelve un tipo anotado con cpsParam o cps se califica como impuro en el documento EPFL. Esto se opone a una expresión pura, que no tiene tipos anotados cps.

Los cálculos impuros se transforman en objetos Shift[A, B, C] (ahora se llama ControlContext[A, B, C] en la biblioteca estándar). Los objetos Shift están extendiendo la mónada de continuación. Su implementación formal se encuentra en el EPFL paper, sección 3.1 página 4. El método map combina un cálculo puro con el objeto Shift. El método flatMap combina un cálculo impuro con el objeto Shift.

El complemento de continuación realiza la transformación del código siguiendo el esquema indicado en la sección 3.4 del EPLF paper. Básicamente, shift se convierten en objetos Shift. Las expresiones puras que se producen después se combinan con mapas, las impuras se combinan con flatMaps (ver más reglas figura 4).Finalmente, una vez que todo se ha convertido hasta el reinicio adjunto, si todo lo que comprueba el tipo, el tipo del objeto Shift final después de todos los mapas y flatMaps debe ser Shift[A, A, C]. La función reset reifica el contenido Shift y llama a la función con la función identidad como argumento.

En conclusión, creo que el documento EPLF contiene una descripción formal de lo que sucede (secciones 3.1 y 3.4 y figura 4). El tutorial que menciono tiene ejemplos muy bien elegidos que dan una gran sensación para continuaciones delimitadas.

Answer 2

Para citar el wikipedia:

una continuación delimitado, continuación componibles o continuación parcial, es una "rebanada" de una trama de continuación que se ha materializado en una función.

sintaxis Scala de esto es:

// Assuming g: X => anything 
reset { 
    A 
    g(shift { (f: (X) => Y) => /* code using function f */ }) 
    B 
} 

Un marco continuación anterior es todo lo que sería ejecutado después de la shift hasta el final del bloque delimitado por reset. Eso incluye llamar a la función g, ya que solo se llamaría después de evaluando shift, más todo el código en B.

No se requiere la función g; en su lugar, podría llamar a un método o ignorar por completo el resultado de shift. Lo muestro para dejar en claro que la llamada shift devuelve un valor que puede usarse.

En otras palabras, ese marco de continuidad se convierte en la siguiente función:

// Assuming g: X => anything 
def f: (X) => Y = { x => 
    g(x) 
    B 
} 

y todo el cuerpo de reposición se convierte en esto:

// Assuming g: X => anything 
A 
def f: (X) => Y = { x => 
    g(x) 
    B 
} 
/* code using function f */ 

Tenga en cuenta que la última sentencia B debe tener un tipo Y. El resultado del cálculo es el resultado de los contenidos del bloque shift, como ocurriría con la traducción anterior.

Si quiere más precisión, check the paper que describe las continuaciones delimitadas en Scala. Los tipos exactos se pueden encontrar en el API documentation.