Kan: Un Lenguaje de Programación Basado en Extensiones de Kan y Teoría de Categorías

Kan aborda el problema fundamental de la verificación de programas y la construcción de sistemas correctos mediante la aplicación directa de la teoría de categorías. En lugar de tratar la verificación como un paso posterior o una capa adicional, Kan integra la corrección matemática en el núcleo del proceso de programación. Esto se logra modelando los programas como diagramas categóricos parciales, donde cada definición es un "generador" y el significado del programa es su "modelo inicial", una extensión de Kan izquierda de los generadores. Este enfoque permite que el compilador "complete el cuerno" (fill the horn), es decir, infiera y genere las partes faltantes del diagrama de manera canónica y universal.

La relevancia de este enfoque radica en su capacidad para transformar la programación de una serie de pasos imperativos o funcionales a una construcción declarativa de propiedades y relaciones. Al basarse en la extensión de Kan, un concepto unificador en la teoría de categorías, el lenguaje promete una base formal robusta para la computación. Esto contrasta con paradigmas tradicionales como el cálculo lambda (centrado en la aplicación) o la programación lógica (centrada en la inferencia), ofreciendo una nueva perspectiva donde la operación primitiva es la "extensión" de un diagrama parcial.

Arquitectura del Sistema

La arquitectura de Kan se centra en un compilador que interpreta los programas como diagramas categóricos. Cada definición en un programa Kan (.kan) se trata como una "fibra" de una construcción de extensión de Kan izquierda. Las definiciones simples (literales) son fibras triviales, mientras que las construcciones más complejas como folds y matches (catamorfismos y anamorfismos) son fibras ricas que representan (co)límites y extensiones de Kan genuinas. El sistema de tipos dependientes de Kan permite expresar propiedades del programa como tipos, y el verificador de tipos (type-checker) demuestra estas propiedades. La terminación de las funciones se garantiza por construcción: el compilador solo acepta recursiones estructurales donde el argumento se reduce en cada llamada, asegurando que si compila, termina.

El compilador de Kan puede operar en varios modos: explain para visualizar cada definición como su fibra categórica, check para verificar la corrección de tipos y propiedades, y build para compilar a código nativo. El compilador "completa el cuerno" (fills the horn) en modo check cuando el objetivo es "contraíble" (contractible), es decir, tiene un único habitante (e.g., Unit -> unit, Id A a a -> refl). En casos con múltiples habitantes (e.g., Nat, Bool), el compilador reporta el objetivo en lugar de adivinar. Kan soporta tipos inductivos de usuario (e.g., List A), tipos de identidad, y una jerarquía de universos. Para la aritmética, distingue entre Nat (tipo inductivo para pruebas) e Integer (tipo de precisión arbitraria para computación eficiente, similar a Python's int), con backends nativos en OCaml y C que garantizan resultados idénticos.

def add : Nat -> Nat -> Nat = lambda m n: match m { | zero => n | suc k => suc (add k n) }

def add_n_zero : (n : Nat) -> Id Nat (add n zero) n = lambda n: match n { | zero => refl | suc k => ap Nat Nat (lambda x: suc x) (add k zero) k (add_n_zero k) }

def fac : Nat -> Integer = lambda n: match n { | zero => 1z | suc k => imul (fromNat (suc k)) (fac k) } eval fac 50

Fundamentos Teóricos

La filosofía de Kan se basa directamente en los trabajos de Daniel Kan sobre las extensiones de Kan y los complejos de Kan, que postulan que un diagrama parcial tiene un "relleno canónico". Este concepto es una generalización fundamental en la teoría de categorías que unifica nociones como límites, colímites, haces (sheaves) y fibraciones. La idea de que "todos los conceptos son extensiones de Kan" (Mac Lane) es central para el diseño del lenguaje. Al integrar estas construcciones categóricas directamente en el sistema de tipos y el compilador, Kan busca proporcionar una base formalmente verificable para la computación, conectando la programación con los fundamentos matemáticos de la teoría de categorías. Esto se alinea con la tradición de lenguajes de programación con tipos dependientes, como Coq o Agda, que permiten la verificación formal de propiedades de programas, pero Kan lo hace a través de una lente categórica explícita.