Un Enfoque Proposicional a la Metodología Abstracting Gradual Typing

TLDR

Esta tesis propone una nuevo enfoque a AGT que utiliza proposiciones lógicas para representar tipos y evidencia, con el objetivo de abordar las limitaciones de AGT en la gestión de dependencias entre tipos. La investigación contribuirá a la teoría y práctica de la tipificación gradual, abriendo nuevas posibilidades para la 
derivación de lenguajes gradualmente tipados con sistemas de tipos complejos.

Introducción

La tipificación gradual se ha convertido en un área de investigación activa en lenguajes de programación, buscando combinar la flexibilidad de los lenguajes dinámicos con las garantías de soundness de los lenguajes estáticos. Una metodología popular para derivar lenguajes gradualmente tipados es *Abstracting Gradual Typing* (AGT), que se basa en la abstracción de tipos para introducir imprecisión. Sin embargo, AGT presenta dificultades al aplicarse a lenguajes con sistemas de tipos complejos que involucran dependencias entre tipos. 

Esta tesis propone una nuevo enfoque a AGT, utilizando **proposiciones lógicas como base para la representación de tipos y evidencia**, con el objetivo de abordar las limitaciones de AGT en la gestión de dependencias entre tipos.

Motivación: Limitaciones de AGT y la Necesidad de una Nuevo Enfoque

AGT se basa en la idea de introducir imprecisión en los tipos mediante la creación de tipos "gradualizados" que representan un rango de posibles tipos concretos. Sin embargo, cuando existen dependencias entre componentes de los tipos, la abstracción individual de cada componente puede resultar en la pérdida de información crucial, **violando propiedades de soundness** del lenguaje original. 

Ejemplo: En el lenguaje de sensibilidad Sax, la propiedad de preservación métrica garantiza que la sensibilidad de una expresión se mantiene acotada. Si se aplica AGT de forma ingenua a Sax, la abstracción de los tipos de sensibilidad podría llevar a la pérdida de información sobre las dependencias entre variables, rompiendo la preservación métrica.

Solución Propuesta:  AGT Basada en Proposiciones

Esta tesis propone utilizar proposiciones lógicas como tipos y evidencia en el proceso de gradualización. Las fórmulas lógicas permiten expresar relaciones complejas entre variables y recursos, capturando las dependencias entre tipos de manera explícita. 

Ventajas de la Aproximación Proposicional:

• Manejo de Dependencias:  Las fórmulas lógicas pueden representar las dependencias entre tipos, evitando la pérdida de información que ocurre al trabajar con evidencias representadas por dos tipos independientes.
• Semántica de Ejecución Clara: La representación de la evidencia basada en fórmulas facilita la definición de una semántica de ejecución de referencia, esencial para la implementación y el análisis de la corrección.
• Soporte para Propiedades de Soundness: La expresividad de las fórmulas lógicas puede ayudar a probar la preservación de propiedades de soundness en el contexto gradual.

Metodología: Gradualizar-Portar-Iterar

Para evaluar la viabilidad y eficacia de la aproximación proposicional, se utilizará la metodología **gradualizar-portar-iterar**:

1. Gradualizar:  Se partirá de un lenguaje con un sistema de tipos estático bien definido y se extenderá con la posibilidad de utilizar tipos graduales.
2. Portar:  Se adaptará la propiedad de soundness clave del lenguaje original al contexto gradual.
3. Iterar: Se iterará sobre el diseño del lenguaje gradual, ajustando la abstracción de tipos y la semántica de ejecución para garantizar que se satisfaga la propiedad de soundness.

Plan de Trabajo

La tesis se desarrollará en las siguientes etapas:

1. Formalización de la Aproximación Proposicional:  Se definirá un marco formal para AGT basada en proposiciones, incluyendo la sintaxis de tipos y evidencia, la semántica de ejecución y las reglas de tipado.
2. Estudio de Caso: Cálculo Lambda Simple: Se aplicará la metodología gradualizar-portar-iterar a un cálculo lambda simple, utilizando proposiciones como tipos y evidencia.
3. Evaluación con Tipos Unión: Se evaluará la aproximación proposicional en un contexto más complejo, como la gradualización de tipos unión.  Se estudiará la interacción entre las proposiciones y la imprecisión introducida por los tipos unión.
4. Aplicación al Lenguaje Sax: Se aplicará la metodología al lenguaje Sax completo, utilizando la experiencia de las etapas anteriores. Se demostrará la preservación métrica en la versión gradual de Sax.

Contribuciones Esperadas

*  Un nuevo marco formal para AGT basada en proposiciones, que permita abordar las limitaciones de AGT en la gestión de dependencias entre tipos.
*  Una demostración de la viabilidad de la aproximación proposicional en diferentes contextos, incluyendo un cálculo lambda simple, tipos unión y el lenguaje de sensibilidad Sax.
*  Un prototipo del lenguaje gradual que permita evaluar su viabilidad práctica.