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

• Autores: Gorka Suárez García
• Directores de la Tesis: Manuel Montenegro Montes (dir. tes.) , Francisco Javier López Fraguas (dir. tes.)
• Lectura: En la Universidad Complutense de Madrid ( España ) en 2022
• Idioma: español
• Tribunal Calificador de la Tesis: Ricardo Peña Marí (presid.) , Jaime Sánchez Hernández (secret.) , Laura M. Castro (voc.) , Josep Francesc Silva Galiana (voc.) , Lars-Ake Fredlund (voc.)
• Enlaces
  • Tesis en acceso abierto en: Docta Complutense
• Resumen
  • español

    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.

  • English

    Type systems are a formal tool that allows the different constructions of a programming language (values, expressions, etc.) to be classified into different categories, called types. Type sustems can detect possible inconsistencies between the different variables and expressions of a program. There are different approaches to applying a type sustem. On the one hand we have languages like C++ with static typing, where type checking is done at compile time, and on the other hand we have languages with dynamic typing like Erlang, where type checking is done at run time. Due to the nature of dynamically typed languages, error detection in programs is done during the testing and debugging phases. However, there are tools that allow the automatic detection os type errors in a program without having to execute it. These tools apply their own static type analysis methodologies to dynamic typing languages...