deft: comprobaciones de tipo opcionales para Janet con tipado gradual

Fuentes: deft: optional type checks for Janet with gradual typing

deft es un módulo para el lenguaje de programación Janet que añade comprobaciones de tipo opcionales aplicables en tiempo de ejecución, en compilación o con anticipación (ahead-of-time). El proyecto aplica los principios del tipado gradual descritos por Siek y Taha, junto con el cálculo de culpa (blame calculus) de Wadler y Findler, lo que permite la interoperabilidad entre código tipado y dinámico dentro del mismo programa.

El sistema incorpora tipos dependientes de predicado (al estilo NQ-Dependent, sin cuantificadores Π ni Σ), tipos compuestos —uniones, intersecciones, ADTs suma sin etiquetar y tipos contenedor—, registros tipados (structs), contratos de orden superior sobre funciones e inferencia bidireccional con unificación. Las anotaciones aparecen en los límites de las llamadas: argumentos al entrar a una función (culpable, el llamante) y valores de retorno al salir (culpable, la función). Tanto los chequeos en frontera como la verificación estática pueden activarse o desactivarse de forma programática.

Deft se integra con Janet mediante el gestor de paquetes jpm —instalación directa, dependencia en project.janet o clonación desde el repositorio en Codeberg— y se importa con un prefijo opcional. Su macro define unificada reemplaza el uso combinado de defn, deftfn, var, ~def y deftval, ofreciendo un tránsito gradual entre código sin tipos y código tipado. La declaración deftype permite crear nuevos tipos a partir de predicados o como combinaciones lógicas de tipos existentes, lo que facilita aproximar uniones, intersecciones y tipos negados sin abandonar la flexibilidad dinámica de Janet.