Un sistema de tipos gradual con semántica de casts para el lenguaje Elixir

Abstract

En este proyecto se desarrolla un sistema de tipos para un fragmento importante de Elixir, un lenguaje de programación funcional de uso industrial con tipado dinámico que se ejecuta sobre la máquina virtual de Erlang. El sistema propuesto tiene la característica de ser algorítmico y estar basado en subtipado estructural. Además, incorpora a su diseño la filosofía del gradual typing, con lo que se hace posible restringir los chequeos de tipo a las porciones anotadas del programa. En el trabajo también se introduce una nueva semántica de evaluación para los programas chequeados con la que se consigue garantizar que el comportamiento de las porciones anotadas del código se preserva durante la ejecución sin cambios con respecto al sistema estático. La semántica se basa en una etapa de inserción de casts de tipo en posiciones críticas del código fuente, que ocurre a posteriori del chequeo de tipos y previo a la compilación. Se presenta también una implementación concreta del sistema de tipos. El proceso de inserción de casts es implementado como una traducción al mismo lenguaje ahora enriquecido con una nueva directiva para casts de tipo, que se consigue representar dentro del lenguaje utilizando las herramientas nativas que Elixir provee para la metaprogramación.