"Improving the Efficiency and Reliability of Gradual Typing" se titula la tesis con que Esteban Allende obtuvo el pasado 8 de enero, el grado de Doctor en Ciencias mención Computación. El trabajo de investigación fue guiado por los académicos del DCC Johan Fabry y Éric Tanter. En tanto, la comisión evaluadora la conformaron los profesores Alexandre Bergel (DCC), David Röthlisberger (Universidad Diego Portales) y, como profesor externo, Laurence Tratt del King’s College London.
Esteban Allende explica que los programadores poseen varias herramientas para evitar errores al momento de programar. Una de ellas son los sistemas de tipos, los que asocian valores con tipos –por ejemplo, asociar el valor 1 con el tipo Entero, y el valor "Una frase" con el tipo Cadena— para luego verificar que un valor recibido o entregado es de un cierto tipo. “Existen dos sistemas de tipos básicos que se ocupan: sistemas de tipos estáticos, en que el programador o el compilador explícitamente señala los tipos esperados de los valores recibidos y que son verificados antes de ejecutar a los programas; y los sistemas de tipos dinámicos, en que el programador no ve los tipos, y estos se ocupan solo cuando se ejecuta el programa para prevenir operaciones no válidas” señala Esteban.
Agrega que los tipos graduales permiten mezclar ambas disciplinas, “es decir, que en ciertas partes de la aplicación se pueda especificar qué tipo de valores se esperan recibir y verificar al compilar o al ejecutar, y que en otras partes no sea necesario especificar ni verificar tipos al compilar”.
En este contexto, el nuevo Doctor explica que el objetivo de su investigación fue, en primer lugar, mejorar la performance de los programas que usan tipos graduales, es decir, que estos corran más rápido al reducir el coste en tiempo de algunos procesos. En segundo lugar, la confiabilidad, esto es poder tener un control de qué partes de la ejecución de los programas están estáticamente tipados y qué partes están dinámicamente tipados. “Esto es más difícil de lo que se puede pensar debido a que las interacciones con otros módulos, funciones, variables, etc., pueden hacer que ciertas secciones interactúen con una sección estáticamente/dinámicamente tipeada sin que el programador se dé cuenta”, dice Esteban y afirma que en su tesis se proponen dos soluciones: estrategias de inserción de casts, que mejora la performance, y tipos graduales acotados (“Confined Gradual Typing”) que se enfoca tanto en la performance como la confiabilidad.
Dentro de los logros obtenidos, destaca, entre otros, el tener un lenguaje gradualmente tipado con una granularidad a nivel expresión. “Al momento de partir mi doctorado, no había ningún lenguaje gradualmente tipado que pudiera usar para mi investigación. Al final, tuvimos que crearlo en lo que más tarde sería Gradualtalk, una de las contribuciones de mi tesis”, señala y agrega que otro importante logro fue trabajar con un problema no resuelto: “Una de nuestras contribuciones es Confined Gradual Typing, que ataca el problema de confiabilidad, problema que encontramos cuando trabajamos en las estrategias de inserción de casts”.
Para la realización exitosa de esta tesis, Esteban destacó el apoyo permanente recibido por los profesores guías: “Johan Fabry siempre me ayudo tanto a mejorar como a corregirme los puntos que estaba equivocándome. El profesor Éric Tanter, era el que me guiaba en la parte teórica de nuestra investigación, y el que expandía las ideas junto a otros profesores”, concluyó.
Resumen "Improving the Efficiency and Reliability of Gradual Typing"
Gradual Typing permite a un programador aplicar tipos estáticos a ciertas partes de un programa, dejando el resto dinámicamente tipeado. Sin embargo, esto viene con un costo en el rendimiento. Una razón es que el runtime tiene que realizar siempre un casteo en el borde entre tipos estáticos y dinámicos. Otra razón es que el borde puede ser creado accidentalmente. Esto también trae un efecto lateral de reducir la fiabilidad del código estático, porque ahora el programador no puede garantizar que su código no arrojará errores de tipo en tiempo de ejecución.
En este trabajo de tesis, mejoramos el rendimiento y la fiabilidad de los programas gradualmente tipeados. Para esto, desarrollamos un lenguaje gradualmente tipeado, Gradualtalk, y luego presentamos dos novedosas ideas: hybrid strategy y Confined Gradual Typing.
La hybrid strategy es una nueva forma de insertar los casts al invocar métodos que combina dos estrategias existentes, permitiendo obtener el mejor rendimiento de ambas. Validamos esta afirmación con benchmarks.
Confined Gradual Typing refina gradual typing con anotaciones para prohibir explícitamente ciertos cruces de frontera entre el código estáticamente y dinámicamente tipeado. Nosotros desarrollamos formalmente dos variantes de CGT que capturan diferentes compromisos entre flexibilidad/garantías. Probamos que CGT es type sound y que las anotaciones ofrecen las garantías esperadas.