Ámbitos como tipos

En PEPM 2016 presentamos el diseño de un lenguaje de restricciones para la verificación de tipos basado en gráficos de alcance. Ese diseño fue la base para el lenguaje de análisis de nombres y tipos NaBL2 que actualmente está integrado en el entorno de trabajo del lenguaje Spoofax. Si bien el enfoque se ocupa elegantemente de una gran variedad de patrones de enlace de nombres, incluida la resolución de nombres dependiente del tipo, se limitó a sistemas de tipos "simples". En particular, NaBL2 no admite sistemas de tipos con tipos estructurales (anónimos) y tipos genéricos (parametrizados). En nuestro artículo OOPSLA 2018 mostramos que estas limitaciones no son intrínsecas al modelo de gráfico de alcance. Mostramos que mediante el uso de ámbitos como tipos, podemos modelar dichos tipos. La imagen muestra el gráfico de alcance para un programa con tipos de registro estructural.

Se presentará la próxima semana en SPLASH 2018 en Boston.

Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser. Ámbitos como tipos. Actas de la ACM sobre Lenguajes de Programación, Volumen 2 Edición OOPSLA, noviembre de 2018, Artículo n.º 114. 10.1145/3276484

Abstracto: Los gráficos de alcance son un marco genérico prometedor para modelar las estructuras de enlace de los lenguajes de programación, mejorar la formalización e implementación, apoyar la definición de verificadores de tipos y la automatización de pruebas de seguridad de tipos. Sin embargo, el trabajo previo sobre grafos de alcance se ha limitado a sistemas simples de tipo nominal. En este artículo, mostramos que la visualización de ámbitos como tipos nos permite modelar la estructura interna de los tipos en una gama de sistemas de tipos no simples (incluidos los registros estructurales y las clases genéricas) utilizando la representación genérica de los ámbitos. Además, mostramos que las relaciones entre estos tipos se pueden expresar en términos de consultas de grafo de alcance generalizado. Ampliamos los gráficos de ámbito con relaciones y consultas de ámbito. Presentamos Statix, un nuevo metalenguaje específico de dominio para la especificación de semántica estática, basado en gráficos de alcance y restricciones. Evaluamos los alcances como enfoque de tipos y el diseño de Statix en casos de estudio de STLCREC, System F y Featherweight Generic Java.