Countable polymorphic may-must effects

Abstract

Muchos programas realizan operaciones tales como mutar el heap, imprimir en pantalla, leer archivos, comunicarse con otros programas o generar números aleatorios. Estas interacciones son conocidas como efectos colaterales. Los efectos son útiles, pero pueden ser problemáticos: un programa podría sobre-escribir un archivo importante, o un programa podría contener logs de depuración en la etapa de producción, exponiendo información interna. Por lo tanto, existen técnicas como los sistemas de tipos y efectos, que nos permiten razonar estáticamente sobre programas con efectos. En esta tesis, proponemos un cálculo formal con un sistema de efectos que permite a los programadores razonar sobre efectos que podrían y que deben suceder cuando un programa se ejecuta. El sistema de efectos diferencia entre efectos que podrían suceder y efectos que deben suceder. Adicionalmente el sistema de efectos nos permite restringir el número de veces que un efecto puede o debe realizarse durante la ejecución de un programa. El lenguaje presentado en esta tesis es llamado lambda mme-p, donde mme representa a los efectos opcionales y a los efectos obligatorios (may-must effects), y p representa efectos polimórficos, efectos genéricos que son representado por variables de efecto, y estas variables pueden ser reemplazadas por efectos concretos. El trabajo de esta tesis consiste en dos partes. En la primera parte, definimos lambda mme-p, un cálculo formal con un sistema de tipo y efectos que combina tanto los efectos que podrían realizarse como los efectos que deben realizarse, y polimorfismo de efectos. La novedad de este trabajo consiste en la combinación de estos conceptos. En la segunda parte, desarrollamos el formalismo de lambda mme-p junto con la definición y prueba de la propiedad de coherencia (soundness) de su sistema de tipo y efectos. La propiedad de coherencia declara que la semántica estática de lambda mme-p es una aproximación acertada de la semántica dinámica, es decir, una función bien tipada respeta la especificación de efectos (sus privilegios y obligaciones). El trabajo realizado se válida mediante la definición y demostración de la propiedad de coherencia. Esta propiedad indica que el lenguaje propuesto tiene sentido, que el lenguaje indica los efectos que podrían y que deben suceder cuando un programa bien tipado se ejecuta. El sistema de tipos y efectos de lambda mme-p, le permite al programador diseñar y cumplir especificaciones mas fuertes de las que son posibles expresar en un sistema de efectos simple. A pesar que lambda mme-p es mas expresivo que un sistema de efectos simple, aun no hay una implementación del lenguaje. lambda mme-p tiene limitantes, tal como la falta de recursión, o tipos dependientes. Por lo tanto, lambda mme-p aun no seria útil para un programador.