¿Se puede utilizar Elementary Affine Logic como el sistema de tipo básico de un lenguaje de programación práctico?

Elementary Affine Logic es un sistema de tipos que captura la clase de términos λ que se pueden reducir en el tiempo elemental. Además, los términos de tipo EAL se pueden reducir utilizando el fragmento abstracto del algoritmo de Lamping, lo cual es particularmente interesante para mí porque estoy explorando los combinadores de interacción correspondientes.

Mi pregunta es, ¿cómo se puede hacer un lenguaje de programación práctico utilizando EAL como sistema de tipos subyacente? Es decir, qué tipo de extensiones (puntos fijos, polimorfismo, tipos dependientes, tipos de datos, etc.) podrían hacerse al sistema de tipos de núcleo sin afectar esa característica, y ¿sería un lenguaje de ese tipo utilizable en la práctica, o sería de alguna manera también? restrictivo por razones que no conozco?

Baillot, Gaboardi y Mogbil intentaron hace unos años algo muy similar, pero utilizando una lógica afín ligera (LAL) en lugar de EAL (puede encontrar el documento aquí ). Creo que su trabajo puede generalizarse fácilmente a EAL, que es un sistema más liberal.

En cuanto a las características de dicho lenguaje, tiene polimorfismo de forma nativa (EAL es una restricción de la lógica lineal de segundo orden). Hasta donde sé, nadie ha mirado los tipos dependientes, pero no veo por qué no deberían funcionar. De hecho, el EAL sin tipo funciona tan bien como el EAL con tipo, porque sus propiedades de normalización no dependen de los tipos.

Una consecuencia es que en EAL puede usar un punto de fijación arbitrario de tipos (ver, por ejemplo, este otro artículo de Baillot) y definir tipos de datos en el estilo recursivo natural (como ), junto con la definición del sistema F menos natural (desde una perspectiva de programación). Sin embargo, por la observación anterior sobre la normalización sin tipo, un lenguaje de programación basado en EAL siempre será total$\mathtt{list\ A := nil\mathrel | A\ *\ list\ A}$, lo que significa que no tendrá un combinador de punto fijo y el uso de tipos recursivos no es tan natural como cabría esperar. Por ejemplo, tome los números de Scott: sin definiciones recursivas (dadas por el combinador de punto fijo) es difícil expresar algo más allá de las operaciones de tiempo constante con esta representación de enteros. Por lo tanto, todavía se tendrá que utilizar los números de la Iglesia para la iteración (es decir, bucles), mediante el uso de lo que se incurrirá en la restricción de la estratificación fundamental de la lógica de luz (lo que les da sus propiedades complejidad): no se puede iterar una función N a t → N a t que se ha definido por iteración ( N a $\mathtt{for}$$\mathsf{Nat}\rightarrow\mathsf{Nat}$$\mathsf{Nat}$ aquí está el tipo de enteros de la Iglesia).

Un ejemplo: con algún "pirateo de enteros de la Iglesia", es posible definir en EAL tal que d b l n _ = 2 n _ sin usar la iteración. Luego, puede iterar d b l para definir la función exponencial e x p que, sin embargo, no puede$\mathsf{dbl}:\mathsf{Nat}\rightarrow\mathsf{Nat}$$\mathsf{dbl}\ \underline{n} = \underline{2n}$ $\mathsf{dbl}$$\mathsf{exp}$en sí ser iterado. Entonces, cualquier lenguaje de programación basado en EAL necesitará algún tipo de mecanismo que prohíba ciertas definiciones por iteración; Es difícil imaginar cómo tal restricción no resultaría en un lenguaje que resulte incómodo para el programador. De todos modos, ¡nadie te prohíbe probar y ver qué puedes conseguir!

En cualquier caso, si está interesado en la relación entre evaluación óptima, EAL y lógicas ligeras en general, le sugiero que eche un vistazo a los documentos de Coppola desde principios hasta mediados de la década de 2000.