Gradual system F

Abstract

El polimorfismo paramétrico es un mecanismo de abstracción ampliamente utilizado en los lenguajes de programación, que permite la definición genérica de funciones y tipos, y proporciona reutilización de código e independencia de representación. Por otra parte, la tipificación gradual permite una transición paulatina entre la comprobación de tipos estática y dinámica basada en anotaciones de tipos controladas por el programador, integrando las ventajas de ambos mundos. Llevar los beneficios del tipado gradual a un lenguaje con polimorfismo paramétrico como el Sistema F, preservando al mismo tiempo la parametricidad relacional, ha resultado ser un gran reto. La dificultad observada en trabajos anteriores se basa en una fuerte tensión entre las dos propiedades deseables de un lenguaje paramétrico gradual, la parametricidad, y la gradualidad, considerando que las funciones pueden intentar utilizar la tipificación gradual para eludir la parametricidad. Los primeros intentos se formularon hace más de una década, y se han propuesto además varios diseños con sintaxis, comportamientos y propiedades variables. Se ha demostrado que, sin tomar precauciones, la parametricidad podría ser violada en un lenguaje gradual. Por esta razón, todos los lenguajes polimórficos graduales propuestos han utilizado alguna forma de mecanismo de sellado/desellado. La idea detrás del sellado/desellado es que un valor sellado con una clave sólo puede ser manipulado por una expresión de desellado que conozca la clave; de lo contrario, se lanza un error. Esta tesis contribuye a la adopción del polimorfismo paramétrico en un lenguaje gradual, preservando la sintaxis del Sistema F y satisfaciendo la gradualidad y parametricidad al mismo tiempo. Exploramos en profundidad la integración de estas dos características derivando dos lenguajes, GSF y Funky. GSF es un lenguaje fuente paramétrico gradual que viola la gradualidad en algunos escenarios. No obstante, establecemos una propiedad más débil que nos permite refutar varias afirmaciones sobre teoremas gratis graduales, aclarando el tipo de razonamiento que admite la parametricidad gradual. Funky es un lenguaje intermedio que va más allá, satisfaciendo plenamente la parametricidad y la gradualidad, y permitiendo la incrustación de diferentes lenguajes fuentes paramétricos graduales. Basándonos en la observación de que la tensión entre gradualidad y parametricidad proviene de la decisión temprana de sellar valores basada en la información de tipo, proponemos el sellado plausible como un nuevo mecanismo de lenguaje intermedio que permite posponer tales decisiones al tiempo de ejecución. Funky soporta el sellado plausible en un entorno simplificado en el que el polimorfismo se restringe a las instancias con tipos base y variables. Aunque los resultados presentados tienen algunas limitaciones, proponen una nueva forma de reconciliar la parametricidad y la gradualidad en un lenguaje con la sintaxis del Sistema F. Además, algunas de nuestras técnicas novedosas son potencialmente reutilizables en otros entornos.