Abstracting gradual typing: Metatheory and applications

Abstract

Han habido muchos enfoques para integrar tipado estático y dinámico. Uno de los enfoques más notables es el del tipado gradual. El enfoque clásico para diseñar lenguajes graduales es usualmente ad-hoc, pero existen metodologías que sistematizan este proceso. Una de ellas es la Abstracting Gradual Typing (AGT), que ayuda a construir sistemáticamente lenguajes graduales a partir de lenguajes estáticamente tipados usando interpretación abstracta al nivel de tipos. A pesar que se a mostrado que AGT a sido efectiva en diferentes contextos, hay aún muchas preguntas abiertas: ¿AGT escala a mecanismos de lenguaje y disciplinas de tipos complejos? ¿Que lenguajes obtienen al usar abstracciones más ricas, o al introducir imprecisión de una manera poco convencional? ¿Cómo se compara el lenguaje gradual resultante con lo existente en la literatura? ¿Que propiedades AGT garantiza de preservar por construcción? ¿Podemos aplicar AGT a un lenguaje gradual derivado con AGT? En esta tesis se trata de responder a estas preguntas, aplicando AGT a disciplinas de tipos y mecanismos de lenguaje complejos. Primero, se aplica AGT a un cálculo lambda con tipado simple y referencias mutables, donde se muestra que una directa aplicación de AGT no garantiza una semántica eficiente respecto al espacio. Se prueba equivalencia contextual con uno de los lenguajes graduales con referencias encontrados en la literatura. Segundo, se aplica AGT a un lenguaje con tipado de seguridad y referencias, introduciendo imprecisión solo en las etiquetas de seguridad de los tipos. Se aprende que una aplicación directa de AGT sólo garantiza preservar por construcción la seguridad de tipos y los criterios refinados de lenguajes graduales. En orden de satisfacer no-interferencia, la propiedad semántica crucial del lenguaje estático, se deben refinar las abstracciones usadas en la semántica dinámica. Pero debido a las referencias mutables, se agrega un chequeo extra en la regla de reducción de asignaciones para prevenir flujos implícitos de información a través de la memoria. Este chequeo extra rompe la garantía gradual dinámica, la cual es parte de los criterios refinados de los lenguajes graduales. Tercero, se aplica AGT para introducir una nueva forma de imprecisión en los tipos, llamada unión gradual, un diseño original de tipos de unión que combina ambos beneficios de uniones etiquetadas y no etiquetadas. Se descubre que las uniones graduales interactúan con el tipo desconocido en una forma que exige un enfoque estratificado para AGT, dependiendo de la composición de dos interpretaciones de abstracción distintas en orden de recuperar optimalidad. Cuarto, se aplica AGT a System F, un lenguaje que soporta polimorfismo paramétrico. Se descubre que una aplicación directa de AGT rompe parametricidad, una propiedad semántica crucial de System F. En orden de recuperar parametricidad, se refinan las abstracciones (y se personalizan ciertas operaciones) usadas en la semántica dinámica. Esta personalización ayuda a preservar parametricidad pero a costa de la violar la garantía gradual dinámica. Esta garantía fue dejada como una conjetura en todos los trabajos previos; aquí se prueba que es simplemente incompatible con la noción clásica de parametricidad. Sin embargo, se establece una propiedad más débil que permite refutar varias afirmaciones acerca de teoremas graduales gratis, clarificando el tipo de razonamiento soportado por la parametricidad gradual.