¿Alguien ha usado la desfuncionalización polimórfica de Pottier y Gauthier en un compilador modular?

La desfuncionalización es una transformación de programa que convierte los programas de orden superior en programas de primer orden. La idea es que, dado un programa, solo hay finitamente muchas abstracciones lambda, por lo que puede reemplazar cada lambda con un id, y cada aplicación de función con una llamada a un procedimiento de aplicación que se ramifica en ese id. Esto a veces se usa en compiladores para lenguajes funcionales, pero su aplicabilidad está limitada por el hecho de que la desfuncionalización es una transformación de todo el programa (debe conocer estáticamente todas las funciones del programa), por lo que solo los compiladores de todo el programa hacen uso de eso.

Sin embargo, Pottier y Gauthier tienen un algoritmo de desfuncionalización de tipo polimórfico dado que utiliza un tipo más sofisticado que involucra GADT. Ahora, dada su codificación, es posible agregar un caso general a su tipo de datos lambda que no es una etiqueta, pero que contiene una función de orden superior. Esto significa que debería ser posible usar su codificación para desfuncionalizar módulo por módulo.

¿Alguien ha hecho esto y me señala un compilador que usa esta idea? (Los compiladores de juguetes están bien, y de hecho son preferidos).

Un enfoque es descrito por

Georgios Fourtounis y Nikolaos S. Papaspyrou. 2013. Soporte de compilación separada en un compilador de desfuncionalización. PIZARRA 2013.

Como @gasche menciona:

Un enfoque diferente en el problema sería considerar que cada módulo puede definir su propio tipo de "funciones desfuncionalizadas" y despachador / manejador.

$n$$i$$0< i < n$$n-i$

Ahora, dada su codificación, es posible agregar un caso general a su tipo de datos lambda que no es una etiqueta, pero que contiene una función de orden superior. Esto significa que debería ser posible usar su codificación para desfuncionalizar módulo por módulo.

¿Podría explicar un poco más sobre lo que quiere decir aquí? No entiendo cómo agregar un caso base (¿sería eso al tipo de datos, a la coincidencia de patrones de la función de envío, o a ambos?) Ayuda a la modularidad en la forma que usted describió; por cierto, ¿por qué te refieres exactamente por "módulo por módulo"?

Me imagino un "caso base" que se utiliza, dentro de un módulo / programa dado, para la desfuncionalización selectiva : tendría un constructor adicional para su tipo de función reified que no es una etiqueta, sino que simplemente integra todas las 'a -> 'bfunciones, de modo que empacar una función en este constructor, en lugar de darle una etiqueta reificada, evitaría su desfuncionalización.

Un enfoque diferente en el problema sería considerar que cada módulo puede definir su propio tipo de "funciones desfuncionalizadas" y despachador / manejador. Las funciones del módulo M1tendrían tipo M1.arrowy se aplicarían usando M1.apply, etc. Si bien eso funciona bien para usos de primer orden de las funciones, no veo muy bien cómo podría extenderlo a una función de orden superior (que no debería tener que sepa de dónde provienen sus argumentos funcionales): si agrupa una función con su despachador, volverá a ingresar al ámbito de las llamadas indirectas a funciones.

Finalmente, en el documento hace referencia a una mención rápida de todo el programa versus el enfoque modular, pero no veo cómo se relaciona con su propuesta. Lo que describen se expresa en términos de "extensiones abiertas" de funciones y tipos de datos (funciones y tipos que podrían definirse en varios módulos independientes). Esto es principalmente una forma ML de describir el hecho de que puede diferir la combinación de análisis / transformaciones de módulos independientes en el momento del enlace, relajando la necesidad de la transformación de todo el programa.