Syl: un lenguaje de programación con tipos dependientes en tiempo de compilación

Fuentes: Syl: A programming language with compile-time dependent types

Syl es un lenguaje de programación diseñado para integrar la computación en tiempo de compilación mediante un sistema de tipos modal, inspirado en la teoría de tipos de dos niveles de András Kovács y los planes para OxCaml. A diferencia de las características de C++, Rust o Zig, que suelen estar restringidas o carecer de un sistema de tipos adecuado, Syl busca codificar la computación en tiempo de compilación de manera más robusta. El sistema de tipos de Syl se basa en dos ejes de modos: la estática y la borración. La estática indica si un valor es conocible en tiempo de compilación, mientras que la borración determina si es conocible en tiempo de ejecución. Este enfoque permite la monomorfización de funciones con parámetros estáticos, optimizando el código generado. Además, Syl implementa tipos dependientes en tiempo de compilación, lo que permite que el tipo del resultado dependa del valor de la entrada, aunque en tiempo de ejecución los tipos se borran y el programa funciona como un lenguaje simplemente tipado. El sistema soporta recursión general en tiempo de compilación, lo que implica que la verificación de tipos no es decidida y que las funciones pueden divergir, pero esto no compromete la seguridad de tipos ni la usabilidad, ya que se aplican límites de combustible para evitar bucles infinitos durante el desarrollo. Syl ofrece una alternativa técnica para programadores interesados en la optimización de compiladores y la teoría de tipos avanzada, manteniendo la intuición de programación de alto nivel.