Reescribir el comprobador de tipos de Futhark: del algoritmo W a un enfoque basado en restricciones

Fuentes: Rewriting the Futhark type checker

Futhark es un lenguaje de programación funcional orientado a la computación paralela sobre arrays. Su comprobador de tipos, sin embargo, ha sido durante años una de las piezas más complejas de mantener, y el autor del lenguaje narra en esta entrada la evolución completa que ha desembocado en un rediseño profundo actualmente en proceso de integración.

El texto recorre las distintas etapas: un primer comprobador muy sencillo, limitado a escalares, arrays, tuplas y funciones de primer orden; la introducción de la inferencia de tipos estilo Hindley-Milner (algoritmo W) con funciones de orden superior; las sucesivas complicaciones derivadas de los registros, los tipos de unicidad y los tipos de tamaño, que provocaban reglas especiales y comportamientos sutiles; y finalmente el punto de inflexión con AUTOMAP, un sistema que automatiza la aplicación de map y que obligó a replantear el diseño por completo.

El nuevo enfoque abandona la comprobación monolítica de una sola pasada y la sustituye por un proceso en fases: resolución de nombres, verificación de consumo y aliasing, y un núcleo basado en generación y resolución de restricciones, inspirado en compiladores como GHC o Flix. La principal ventaja es que se difieren las decisiones hasta disponer de toda la información, lo que facilita el manejo de características avanzadas y la depuración. La entrada reflexiona sobre las lecciones aprendidas en el camino y deja entrever que el reemplazo del antiguo comprobador promete un código más claro y mantenible, aunque la culminación de AUTOMAP sigue siendo trabajo futuro.