Análisis estático de tipos para lenguajes de tipado dinámico

Resumen

Los sistemas de tipos son una herramienta formal que permiten clasificar las distintas construcciones de un lenguaje de programación (valores, expresiones, etc.) en distintas categorías, llamadas tipos. Con ello se pretende detectar posibles inconsistencias entre las distintas variables y expresiones de un programa. Existen distintos enfoques en la aplicación de un sistema de tipos. Por un lado tenemos lenguajes como C++ con tipado estático, donde la comprobación de tipos se realiza en tiempo de compilación, y por el otro tenemos los lenguajes con tipado dinámico como Erlang, donde la comprobación de tipos se realiza en tiempo de ejecución. Como consecuencia de la naturaleza de los lenguajes de tipado dinámico, la detección de errores en los programas se realiza durante las fases de prueba y depuración. No obstante, existen herramientas que permiten la detección automática de errores de tipo en un programa sin necesidad de ejecutarlo. Estas herramientas aplican metodologías propias de análisis estático de tipos a lenguajes de tipado dinámico. Erlang es un lenguaje de programación funcional concurrente de tipado dinámico, que dispone de una herramienta propia (Dialyzer) para analizar programas escritos en Erlang y poder detectar, en tiempo de compilación, discrepancias en el uso de los tipos. Esta herramienta se basa en la noción de success types, que son una sobreaproximación a la semántica de las expresiones del lenguaje, de modo que la evaluación de una expresión mal tipada necesariamente fallará en tiempo de ejecución. Dialyzer permite a un programador especificar tipos polimórficos (que capturan relaciones entre las entradas y la salida de una función) y tipos sobrecargados (que permiten reflejar las distintas ramas de ejecución de una función). No obstante, la información relativa al polimorfismo y sobrecarga solamente sirve a efectos de documentación de los programas, y Dialyzer descarta esta información a la hora de realizar su comprobación de tipos. Esto supone una pérdida de precisión en el análisis, lo cual se traduce en una menor capacidad para detectar errores en un programa. En esta tesis presentamos un sistema de tipos polimórficos sobrecargados, basado en la noción de success types, con el que poder analizar programas escritos en un subconjunto del lenguaje Erlang. Gracias al polimorfismo podemos conectar con mayor precisión las entradas y salidas de un tipo funcional a la hora de sobreaproximar la semántica de las funciones. Además, al incorporar sobrecarga, podemos capturar de un modo más preciso la distinción entre las ramas de ejecución que pueden darse al evaluar una expresión. Al disponer de ambas características, conseguimos realizar un análisis de tipos más preciso que el realizado por el sistema de success types monomórfico de Dialyzer. Además de describir un sistema para derivar success types polimórficos sobrecargados, también presentamos un algoritmo de inferencia acompañado de una herramienta que infiere y muestra los success types de un conjunto de funciones dado. En particular, hemos utilizado esta herramienta para inferir los tipos de algunas funciones habituales en programación funcional. En esta tesis no solo presentamos un sistema de success types polimórficos sobrecargados con el que derivar e inferir tipos, sino que también aportamos resultados de corrección que demuestran que los tipos obtenidos son success types de las expresiones analizadas. Esto es importante, ya que Dialyzer carecía de un marco teórico sólido sobre el que poder razonar a la hora de incorporar tipos polimórficos. De hecho, esta carencia ha sido la que ha motivado gran parte de nuestra investigación, que procura ofrecer unos fundamentos teóricos para futuros sistemas de tipos basados en success types.