Tipos Dependientes en Tiempo de Compilación: Un Enfoque Modal para Programación de Sistemas

El problema fundamental que Syl busca resolver es la brecha entre la expresividad y la seguridad de los sistemas de tipos avanzados (como los tipos dependientes) y la necesidad de rendimiento y control de bajo nivel en la programación de sistemas. Lenguajes como C++, Rust y Zig han introducido características limitadas para la computación en tiempo de compilación (templates, const generics, comptime), pero carecen de un sistema de tipos unificado y formal para gestionar estas capacidades. Syl propone un sistema de tipos modal, inspirado en la teoría de tipos de dos niveles, para integrar de manera coherente la computación en tiempo de compilación con la verificación de tipos.

La motivación es permitir que las propiedades de los programas, como las longitudes de los vectores o las variantes de un intérprete, se verifiquen y se utilicen para la especialización del código en tiempo de compilación. Esto no solo mejora la seguridad al prevenir errores lógicos antes de la ejecución, sino que también permite optimizaciones significativas al generar código altamente especializado. La capacidad de 'monomorfizar' funciones basadas en valores estáticos o 'borrados' es clave para lograr un rendimiento comparable al de las especializaciones de plantillas de C++, pero con la robustez de un sistema de tipos formal.

Arquitectura del Sistema

Syl introduce un sistema de tipos modal donde cada valor tiene un 'modo' además de un 'tipo'. Los modos se definen en dos ejes: 'staticity' (estático/dinámico) y 'erasure' (borrado/no borrado). Un valor 'estático' es conocido en tiempo de compilación, mientras que uno 'dinámico' no lo es. Un valor 'no borrado' es conocido en tiempo de ejecución, mientras que uno 'borrado' no lo es. Por ejemplo, los literales son 'estáticos no borrados'.

El sistema permite una relación de 'sub-moding' donde un valor estático puede tratarse como dinámico, y uno no borrado como borrado, pero no al revés. Las funciones que operan sobre parámetros 'estáticos' o 'borrados' pueden ser monomorfizadas, lo que significa que el compilador genera implementaciones especializadas para cada valor de entrada estático. Esto es análogo a la especialización de plantillas en C++ o la desvirtualización de llamadas a funciones. La clave es que las expresiones 'if erased' o 'match erased' se resuelven completamente en tiempo de compilación, permitiendo que las ramas de código no alcanzables se eliminen del binario final.

Los tipos dependientes se logran permitiendo que el tipo de retorno de una función dependa del valor de sus argumentos estáticos. Por ejemplo, una función puede retornar un 'int' si un argumento booleano estático es 'true', y un 'bool' si es 'false'. Syl es dependientemente tipado en tiempo de compilación y simplemente tipado en tiempo de ejecución, lo que significa que las construcciones que determinan la forma del programa en tiempo de ejecución requieren información 'estática'. Los tipos son siempre 'borrados', por lo que el programa en tiempo de ejecución no puede inspeccionar los tipos. El compilador de Syl implementa la verificación de tipos dependientes de manera similar a lenguajes existentes, pero con la particularidad de permitir recursión general en las computaciones de tiempo de compilación, lo que implica que la verificación de tipos no es decidible y no garantiza la terminación de las pruebas.

let f = fn (static x : bool) -> print_bool x;;
f true;;
f false;;

let f = fn (erased x : bool) -> if erased x then print_int 0 else print_int 1;;
f true;;
f false;;

let f = fn (erased x : bool) -> if erased x then 0 else true;;
let x = (f true) : int;;
let y = (f false) : bool;;

let nat =
  fun nat (erased _ : unit) : erased type =
    variant { zero, succ : &(nat ()) }
  in
  nat ()
;;

fun add (static nm : nat ^ nat) : nat =
  match static nm {
    (.zero, m) -> m,
    (.succ &n, m) -> nat.succ box (add (n, m)),
  }
;;

Fundamentos Teóricos

La base teórica de Syl se encuentra en la teoría de tipos de dos niveles, un concepto explorado por András Kovács y los planes para OxCaml. Esta teoría distingue entre un nivel de 'tipos' (que describen la estructura del programa) y un nivel de 'términos' (los valores del programa), y cómo la información puede fluir entre estos niveles. La idea central de la compilación por etapas con teoría de tipos de dos niveles, aunque no siempre presentada como un sistema de tipos modal, es directamente relevante para el diseño de Syl.

La decisión de permitir recursión general en las computaciones de tiempo de compilación y de tener type : type en Syl se alinea con la discusión sobre la irrelevancia, la igualdad heterogénea y los sistemas de tipos dependientes call-by-value, como se explora en trabajos académicos que abordan las implicaciones de estas características en la decidibilidad de la verificación de tipos y la capacidad de los tipos para actuar como pruebas. Aunque esto difiere de lenguajes de prueba de teoremas como Lean o Agda, que requieren terminación y totalidad para garantizar la validez de las pruebas, Syl prioriza la flexibilidad para la programación de sistemas, gestionando la no terminación con límites de 'fuel' en el compilador.