Gradual typing for generic type-and-effect systems

Abstract

Los sistemas de tipos-y-efectos (type-and-effect systems) permiten a los programadores hacer valer invariantes y restricciones sobre los efectos secundarios que se generan durante la evaluación de un programa. Los sistemas de tipos-y-efectos consideran efectos secundarios tales como estado, excepciones y E/S, entre otros. Desafortunadamente, los sistemas de tipos-y-efectos también obligan al programador a introducir anotaciones de efectos, lo que implica un esfuerzo adicional. En la práctica, los sistemas de tipos-y-efectos no son comúnmente usados. Conjeturamos que una de las razones importantes para la limitada adopción de los sistemas de efectos son las dificultades para realizar la transición desde un sistema donde los efectos secundarios son implícitos hacia una disciplina de efectos totalmente estática. Los tipos graduales (Gradual typing) permiten a los programadores combinar la flexibilidad de los lenguajes dinámicamente tipados con las garantías provistas por los sistemas de tipos estáticos. En lenguajes con tipos graduales, las anotaciones de tipos son parte del lenguaje, pero no son obligatorias. Un sistema de tipos gradual utiliza la información disponible para proveer garantías estáticas, rechazando los programas claramente incoherentes, e introduce verificaciones en tiempo de ejecución cuando la información estática no es suficiente para aceptar o rechazar definitivamente un programa. Esta tesis demuestra que las ideas de diseño detrás de los tipos graduales pueden aplicarse a los sistemas de tipos-y-efectos, tanto para aumentar la expresividad de estos sistemas así como para proveer flexibilidad para migrar programas con efectos secundarios impl ́ıcitos e irrestrictos hacia programas con una disciplina de efectos completamente estática. Se adaptaron ideas de tipos graduales para introducir verificación gradual de efectos para sistemas de tipos-y-efectos. La verificación gradual de efectos habilita al programador para decidir dónde y cuándo introducir anotaciones de efectos, agregando verificaciones en tiempo de ejecución cuando las anotaciones estáticas son insuficientes. Para evitar redefinir la verificación gradual de efectos para cada disciplina de tipos-y-efectos, introducimos verificación gradual de efectos para una plataforma genérica de tipos-y-efectos, en la que se puede instanciar cualquier disciplina de efectos monotónica, produciendo un sistema coherente. Presentamos la verificación gradual de efectos basándonos en conceptos de interpretación abstracta para construir la verificación gradual de efectos genérica. Utilizando verificación gradual de efectos genérica, introducimos tipos graduales para sistemas de tipos-y-efectos: un sistema donde las anotaciones de efectos y de tipos no son obligatorias, y donde se introducen verificaciones en tiempo de ejecución y casts cuando la información estática no es suficiente para asegurar la coherencia de un programa. De la manera definida, los tipos graduales para sistemas de tipos-y-efectos permiten migrar desde sistemas carentes de anotaciones de efectos o de tipos hacia una disciplina estática de tipos-y-efectos de manera segura.