Countable polymorphic may-must effects

Tesis para optar al grado de Magíster en Ciencias, Mención ComputaciónMemoria para optar al título de Ingeniero Civil en ComputaciónMuchos 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.Proyecto FONDECYT Regular 115001