types - ¿El rompecabezas de las continuación de yin yang tiene sentido en un lenguaje tipado?

functional-programming scheme

Question

Esta pregunta está relacionada con "¿Cómo funciona el rompecabezas yin-yang?" . El ejemplo de yin yang de continuaciones en el esquema se ve así, según el artículo de Wikipedia :

(let* ((yin
     ((lambda (cc) (display #/@) cc) (call-with-current-continuation (lambda (c) c))))
   (yang
     ((lambda (cc) (display #/*) cc) (call-with-current-continuation (lambda (c) c)))))
(yin yang))

Estoy tratando de escribir una pieza equivalente de código en un lenguaje (editado: estáticamente ), como SML / NJ, pero me está dando errores de tipeo. Entonces, o bien el acertijo no escribe, o estoy malinterpretando la sintaxis del esquema. ¿Cómo se vería el fragmento de código anterior en SML u Ocaml (con extensión callcc )?

Por cierto, ¿cuál es la fuente del rompecabezas? ¿De dónde vino?

Editar: creo que sé la respuesta. Necesitamos un tipo recursivo t satisfaga t = t -> s para algunos tipos s .

Edición de edición: No, no, la respuesta es un tipo recursivo que satisface t = t -> t .

Answer 1

Creo que voy a responder mi propia pregunta. Mostraré dos soluciones, una en eff y otra en Ocaml.

eff

Vamos a trabajar con eff (estoy sonando aquí mismo, mire abajo para otra forma en OCaml con la extensión de delimitación de Oleg ). La solución se explica en el documento Programación con efectos algebric y continuaciones .

Primero definimos shift y reset en eff:

type (''a, ''b) delimited =
effect
  operation shift : ((''a -> ''b) -> ''b) -> ''a
end

let rec reset d = handler
  | d#shift f k -> with reset d handle (f k) ;;

Aquí está el rompecabezas del yin yang transcrito en eff:

let y = new delimited in
  with reset y handle
    let yin = (fun k -> std#write "@" ; k) (y#shift (fun k -> k k)) in
    let yang = (fun k -> std#write "*" ; k) (y#shift (fun k -> k k)) in
      yin yang

Pero eff se queja de que no puede resolver la ecuación de tipo α = α → β. En la actualidad, eff no puede manejar tipos recursivos arbitrarios, por lo que estamos estancados. Como forma de hacer trampa, podemos desactivar la comprobación de tipos para ver si, como mínimo, el código hace lo que se supone que debe:

$ eff --no-types -l yinyang.eff
@*@**@***@****@*****@******@*******@********@*********@*******...

Ok, está haciendo lo correcto, pero los tipos no son lo suficientemente potentes.

OCaml

Para este ejemplo, necesitamos la biblioteca delimcc de Oleg Kiselyov . El código es el siguiente:

open Delimcc ;;

let y = new_prompt () in
  push_prompt y (fun () ->
    let yin = (fun k -> print_string "@" ; k) (shift y (fun k -> k k)) in
    let yang = (fun k -> print_string "*" ; k) (shift y (fun k -> k k)) in
      yin yang)

Nuevamente, Ocaml no compilará porque golpea una ecuación de tipo recursiva. Pero con la opción -rectypes podemos compilar:

ocamlc -rectypes -o yinyang delimcc.cma yinyang.ml

Funciona como se esperaba:

$ ./yinyang
@*@**@***@****@*****@******@*******@********@*********@...

OCaml calcula que el tipo de yin y yang es (''a -> ''a) as ''a , que es su manera de decir "un tipo α tal que α = α → α". Este es precisamente el tipo característico de los modelos de cálculo λ sin tipo. Así que ahí lo tenemos, el rompecabezas yin yang esencialmente utiliza características del cálculo λ no tipado .

Answer 2

Es posible declarar un tipo funcional recursivo en C #, un lenguaje de tipo estático:

delegate Continuation Continuation(Continuation continuation);

Esta definición es equivalente a α : α → α ML.

Ahora podemos "traducir" el rompecabezas yin-yang en C #. Esto requiere una transformación para la llamada / cc, y necesitamos hacer la transformación dos veces porque hay dos, pero el resultado se parece mucho al original y todavía tiene una llamada yin(yang) :

Continuation c1 = cc1 =>
{
    Continuation yin = new Continuation(arg => { Console.Write("@"); return arg; })(cc1);
    Continuation c2 = cc2 =>
    {
        Continuation yang = new Continuation(arg => { Console.Write("*"); return arg; })(cc2);
        return yin(yang);
    };
    return c2(c2);
};
c1(c1);

Claramente ahora, la variable yang está solo en el ámbito local, por lo que podemos optimizarla:

Continuation c1 = cc1 =>
{
    Continuation yin = new Continuation(arg => { Console.Write("@"); return arg; })(cc1);
    Continuation c2 = cc2 => yin(new Continuation(arg => { Console.Write("*"); return arg; })(cc2));
    return c2(c2);
};
c1(c1);

Ahora, nos damos cuenta de que esas pequeñas funciones en línea realmente solo generan un carácter y de lo contrario no hacen nada, por lo que podemos desenvolverlos:

Continuation c1 = cc1 =>
{
    Console.Write("@");
    Continuation yin = cc1;
    Continuation c2 = cc2 =>
    {
        Console.Write("*");
        return yin(cc2);
    };
    return c2(c2);
};
c1(c1);

Finalmente, queda claro que la variable yin es redundante (podemos usar cc1 ). Sin embargo, para preservar el espíritu original, cambie el nombre de cc1 a yin y cc2 a yang y recuperemos nuestro adorado yin(yang) :

Continuation c1 = yin =>
{
    Console.Write("@");
    Continuation c2 = yang =>
    {
        Console.Write("*");
        return yin(yang);
    };
    return c2(c2);
};
c1(c1);

Todos los anteriores son el mismo programa, semánticamente. Creo que el resultado final es un fantástico rompecabezas de C # en sí mismo. Así que respondería a su pregunta diciendo: sí, claramente tiene mucho sentido incluso en un lenguaje de tipo estático :)

Answer 3

_{Ver también mi respuesta a cómo funciona el rompecabezas yin yang , que tuve que encontrar una respuesta antes de poder responder a este.}

Ser un lenguaje "mecanografiado" no significa, por sí solo, la diferencia si este acertijo es expresable en él (sin importar cuán vago sea el término "lenguaje escrito"). Sin embargo, para responder a su pregunta más literalmente: sí, es posible, porque Scheme en sí es un lenguaje tipado: cada valor tiene un tipo conocido. Evidentemente, esto no es lo que quiso decir, así que supongo que quiere decir si esto es posible en un idioma en el que a cada variable se le asigna un tipo permanente que nunca cambia (también conocido como "lenguaje tipado estáticamente").

Además, supondré que desea preservar el espíritu del rompecabezas cuando se expresa en algún idioma. Obviamente, es posible escribir un intérprete de Scheme en un código de máquina x86, y obviamente es posible escribir un intérprete de código de máquina x86 en un lenguaje tipeado que solo tenga tipos de datos enteros y punteros a las funciones. Pero el resultado no está en el mismo "espíritu". Para hacer esto más preciso, colocaré un requerimiento adicional: el resultado debe expresarse usando continuidades verdaderas. No es una emulación, sino continuas completas.

Entonces, ¿puedes tener un lenguaje estáticamente tipado con continuaciones? Resulta que puedes, pero igual puedes llamar trampa. Por ejemplo, en C #, si mis continuaciones se definieron como "función que toma un objeto y devuelve un objeto", donde "objeto" es un tipo que puede contener cualquier cosa, ¿lo encontrará aceptable? ¿Qué pasa si la función toma y devuelve una "dinámica"? ¿Qué sucede si tengo un lenguaje "mecanografiado" en el que cada función tiene el mismo tipo estático: "función", sin definir los tipos de argumentos y los tipos de devolución? ¿Sigue el programa resultante en el mismo espíritu, aunque utiliza verdaderas continuaciones?

Mi punto es que la propiedad "tipo estáticamente" todavía permite una gran cantidad de variación en el sistema de tipos, lo suficiente como para marcar la diferencia. Entonces, solo por diversión, consideremos qué tipo de sistema necesitaría soportar para calificar como no engañoso por cualquier medida.

La call/cc(x) operador call/cc(x) también se puede escribir como x(get/cc) , que es mucho más fácil de comprender en mi opinión. Aquí, x es una función que toma una Continuación y devuelve un valor, mientras que get/cc devuelve una Continuation . Continuation tiene todos los rasgos de una función; se puede invocar con un argumento y sustituirá el valor transferido a donde get / cc que lo creó originalmente se ubique, reanudando la ejecución en ese punto.

Esto significa que get / cc tiene un tipo incómodo: es una function , pero la misma ubicación eventualmente devolverá un valor cuyo tipo aún no conocemos. Supongamos, sin embargo, que en el espíritu de los lenguajes de tipo estático, requerimos que se repare el tipo de devolución. Es decir, cuando llama al objeto de continuación, solo puede pasar valores de un tipo predefinido. Con este enfoque, el tipo de la función de continuación se puede definir con la expresión recursiva de la forma T = function T->T Como señaló un amigo, este tipo puede ser realmente declarado en C #: public delegate TT(T t); !

Entonces ahí lo tienes; ser "mecanografiado" no excluye ni garantiza que pueda expresar este acertijo sin alterar su naturaleza. Sin embargo, si permite el tipo estático "puede ser cualquier cosa" (conocido como object en Java y C #), entonces la única otra cosa que necesita es soporte para verdaderas continuaciones, y el rompecabezas puede representarse sin problemas.

Al abordar la misma pregunta desde una perspectiva diferente, considere mi reescritura del acertijo en algo más parecido a un lenguaje imperativo de tipo estático tradicional, que expliqué en la respuesta vinculada :

yin = (function(arg) { print @; return arg; })(get-cc);
yang = (function(arg) { print *; return arg; })(get-cc);
yin(yang);

Aquí, el tipo de yin y yang nunca cambia . Siempre almacenan una "continuación C que toma una C y devuelve una C" . Esto es muy compatible con el tipado estático, cuyo único requisito es que el tipo no cambie la próxima vez que ejecute ese código.