- La teoría de tipos dependientes incluye objetos de prueba, pero el autor la considera una estructura innecesaria e ineficiente
- Estudió directamente sistemas históricos basados en tipos dependientes como AUTOMATH y el sistema formal de Martin-Löf, pero Isabelle evolucionó como un marco lógico genérico
- Isabelle/HOL, basado en la teoría de tipos simples (lógica de orden superior), destaca en automatización, bibliotecas a gran escala y legibilidad
- A través del proyecto ALEXANDRIA, demostró que incluso solo con lógica de orden superior es posible la formalización de teoremas matemáticos avanzados
- A pesar de la madurez de sistemas de tipos dependientes como Lean, el autor sigue prefiriendo la practicidad del enfoque de lógica de orden superior por los problemas de rendimiento y complejidad
Tipos dependientes y objetos de prueba
- En la teoría de tipos dependientes, los objetos de prueba (proof objects) son indispensables, pero el autor los considera un desperdicio de espacio
- En la arquitectura LCF, solo pueden ejecutarse pasos de prueba válidos mediante verificación de tipos al nivel del lenguaje de implementación, no dentro de la lógica
- Gracias a una idea de Robin Milner, se introdujo el concepto de proof kernel, que se convirtió en la base de Isabelle
- A la pregunta de por qué “no usó tipos dependientes”, el autor responde: “los usé durante mucho tiempo”
Experiencia con AUTOMATH
- En 1977, en Caltech, asistió a una clase de N. G. de Bruijn sobre AUTOMATH, aunque no pudo usar el sistema directamente
- En ese momento, el sistema de la Universidad de Eindhoven no estaba conectado a ARPAnet y además se necesitaba una computadora basada en ALGOL 60
- AUTOMATH es un sistema de tipos dependientes, pero no implementa la correspondencia Curry–Howard
- El usuario tenía que añadir como axiomas los símbolos y reglas de inferencia de la lógica que quisiera usar
- de Bruijn lo comparaba con un “gran restaurante que ofrece toda clase de comida”
- Isabelle retomó esa idea y buscó la generalidad como marco lógico
- Sin embargo, de Bruijn detestaba la teoría de conjuntos y veía las matemáticas como algo esencialmente basado en tipos
- El autor cuestionó la verificación de corrección de AUTOMATH; de Bruijn le envió un tratado de teoría del lenguaje (300 páginas), pero no le resultó satisfactorio
Teoría de tipos de Martin-Löf
- En la Universidad Chalmers de Gotemburgo, investigó la teoría de tipos de Martin-Löf y quedó fascinado por la posibilidad de la síntesis de programas
- La valoró como claramente “correcta” por implementar directamente los principios de la lógica intuicionista de Heyting
- Trabajó en ello durante años e implementó una versión inicial de Isabelle sobre la teoría de Martin-Löf
- Aún hoy se incluye en la distribución como Isabelle/CTT
- Sin embargo, la investigación se vino abajo por el ambiente dogmático centrado en Per Martin-Löf y por el giro forzado hacia la igualdad intensional (intensional equality)
- Sistemas posteriores como Calculus of Constructions (CoC), Rocq y Lean dejaron las mismas dudas
- CoC pasó décadas acumulando diversas variantes y axiomas opcionales
Elecciones de investigación y rumbo de Isabelle
- Los investigadores deben elegir entre desarrollar un nuevo sistema formal o ampliar y aprovechar uno existente
- Isabelle fue diseñado como un marco generalizado capaz de admitir distintas lógicas
- En 1985, Mike Gordon realizó verificación de hardware con la teoría de tipos simples de Church
- Más adelante, John Harrison ideó una codificación para la dimensión de vectores
- Isabelle/HOL añadió a la teoría de Church clases de tipos axiomáticas y el sistema modular locale
- La comunidad de Lean logró una enorme formalización matemática (mathlib) basada en CoC
El proyecto ALEXANDRIA y la prueba de los límites de la lógica de orden superior
- El proyecto ALEXANDRIA, financiado por el ERC, destacó la automatización, las bibliotecas y la legibilidad de Isabelle
- Al principio se esperaba que la lógica de orden superior tuviera límites, pero en la práctica se formalizaron con éxito matemáticas avanzadas como los esquemas de Grothendieck
- Paulo Emílio de Vilhena y Martin Baillon demostraron que todo cuerpo tiene una extensión algebraicamente cerrada
- El proyecto se amplió hasta resultados avanzados como el teorema de Balog–Szemerédi–Gowers
- La afirmación de que “sin tipos dependientes es imposible formalizar matemáticas” desapareció, y solo quedó la idea de que “con tipos dependientes queda más limpio”
Lean y la postura actual sobre los tipos dependientes
- El autor envidia el tamaño de la comunidad de Lean y su herramienta Blueprint, pero los problemas de rendimiento y complejidad siguen ahí
- Se reportan repetidamente choques con la igualdad intensional y la dificultad de decidir cuándo usar tipos dependientes
- El autor compara los tipos dependientes con el Full Self-Driving de Tesla, señalando la expectativa excesiva y la incomodidad real
Apéndice: límites teóricos de la lógica de orden superior
- Algunos sostienen que la lógica de orden superior es débil desde el punto de vista de la teoría de la prueba, pero eso solo significa que es más débil que la teoría de conjuntos ZF
- Según los resultados de ALEXANDRIA, incluso con lógica de orden superior pueden tratarse estructuras matemáticas complejas como los esquemas de Grothendieck
- Solo dos demostraciones requirieron añadir axiomas de ZF, y eran precisamente teoremas que mencionaban directamente objetos de ZF
Notas al pie
- El intuicionismo es una filosofía que considera el lenguaje como algo más que un simple medio de registro, y no es lo mismo que la matemática constructiva (constructive mathematics) de hoy
1 comentarios
Opiniones de Hacker News
Los tipos dependientes (dependent types) son muy útiles en ciertas situaciones
Por ejemplo, sería bueno que Python pudiera expresar y verificar con tipos una “matriz
float32de tamaño 10×5”Pero conceptos como la correspondencia Curry–Howard resultan confusos desde la perspectiva humana
Un error de tipos se siente como una simple equivocación que se puede corregir, pero un error de prueba es un problema mucho más complejo que requiere razonamiento
Por eso, considero que la verdadera fortaleza de Lean no es su sistema de tipos, sino la comunidad y la estructura open source de mathlib
Mientras que el AFP de Isabelle funciona más como una revista académica, en Lean la colaboración basada en pull requests es muy activa
Actualmente estoy desarrollando un nuevo demostrador de teoremas, Acorn(acornprover.org), con la intención de combinar las ventajas de Lean e Isabelle
La expresividad simple de los tipos dependientes en Lean es buena, pero cuando se usan demasiado a fondo se vuelven difíciles de depurar
Sin embargo, no se puede garantizar en tiempo de compilación el rango de un índice que solo se conoce en tiempo de ejecución
Un verdadero lenguaje con tipos dependientes puede evitar errores en tiempo de ejecución a nivel de tipos
De hecho, incluso en lenguajes con tipos dependientes rara vez se usan para evitar errores en tiempo de ejecución;
se utilizan más bien para invariantes de estructuras de datos o para verificar programas después de definirlos
Referencias relacionadas: FAQ sobre división por cero en teoría de tipos, presentación de Xavier Leroy
Por ejemplo, como en la línea 38 de este código, se puede expresar el tamaño de una matriz mediante tipos
También implementé la definición del tipo vector y el tipo resultado de la multiplicación de matrices
Sin embargo, solo lo estoy probando a nivel de proyecto personal, y puede que no sea adecuado para proyectos de datos a gran escala
Esto se relaciona con el concepto de Propositions as Types
Me da curiosidad cómo funcionan los tipos dependientes en tiempo de ejecución, y si se necesitan tanto compilación como verificación de tipos en runtime
También me pregunto si al implementarlos no aparece la complejidad de tener muchas indirecciones
El argumento del Dr. Paulson no es que los tipos dependientes sean malos, sino que no son imprescindibles
Habría estado bien ver más discusión sobre los problemas de rendimiento de Lean o sobre la igualdad intensional (intensional equality)
Casos como HEq en Isabelle(enlace), donde no hay igualdad definicional, causan problemas
Por eso creo que es mejor usar tipos dependientes lo menos posible
Incluso en sistemas sin tipos estáticos como ACL2 se puede verificar bastante bien
Al final, lo importante es el equilibrio entre practicidad y verificabilidad
Lean y Agda todavía se usan menos en verificación a escala industrial
También es interesante comparar Concrete Semantics(enlace) y Logical Verification 2025(enlace)
En la práctica, los refinement types podrían ser más útiles
Ejemplos: Rust Creusot, Dafny y este ejemplo de prueba de leftpad en LiquidHaskell
Pero en verificación de programas hacen falta lemas auxiliares complejos, como “dos pruebas son iguales”, y muchas veces eso no se puede demostrar
Lo importante no es si una característica es necesaria para existir, sino qué tan útil es
Al final, elegir una herramienta es cuestión de preferencia del desarrollador y eficiencia
Es interesante que gran parte de los debates en lógica moderna termine reduciéndose a preferencias estéticas
Si las ventajas prácticas fueran realmente abrumadoras, no habría tanto debate
Como referencia, el artículo de Paulson y Lamport de 1999 “Typing in Specification Languages” vale mucho la pena
Después también evolucionaron enfoques de formalismo informal como el TLA+ de Lamport
A cambio de obtener garantías en tiempo de compilación, pagas el precio de mayor complejidad y tiempos de build más largos
La pregunta clave es si ese intercambio vale la pena
El problema de HOL (teoría de tipos simple) no es la dependencia, sino la falta de fuerza lógica
Esto equivale a una versión restringida de la teoría de conjuntos de Zermelo, y es demasiado débil para formalizar por completo las matemáticas modernas
En particular, es difícil manejar problemas de tamaño en áreas como la teoría de categorías (category theory)
Me pregunto cuánto difiere eso del estilo de trabajo de los matemáticos reales
Por ejemplo, si se añade un ‘inaccessible cardinal’, se vuelve parecido al concepto de ‘universe’ en teoría de tipos
Yo me especialicé en métodos formales y me parecían geniales los tipos dependientes, pero en la práctica su uso fue siempre una batalla cuesta arriba
Cuando usaba F#, intenté introducir F*, pero a mis colegas les pesaba mucho la curva de aprendizaje matemática
Al final llegué a la conclusión cínica de que los ingenieros no suelen aprender bien herramientas con mucha matemática
Aprovecha la resolución de restricciones basada en SMT para permitir un uso ligero de tipos dependientes
Pero no responde preguntas filosóficas como “¿esto es realmente correcto?”
El mundo de la prueba matemática y el de la verificación de software son bastante distintos
Al final, el tiempo es limitado
En nuestra empresa, Phosphor, estamos experimentando con la combinación de tipos dependientes y consultas de bases de datos/grafos
Eso nos permitió compensar las limitaciones de RDF y construir un sistema de consultas basado en lógica
En la práctica usamos TypeDB(typedb.com), y nos ha resultado más rápido que MongoDB y útil para modelar datos complejos
También se parece al concepto de ontology de Palantir
Al final, el secreto de los tipos dependientes parece ser saber cuándo no usarlos
Más que criticar a Lean o Rocq, me hace pensar que quizá en algunos casos conviene un enfoque al estilo de Isabelle
El proyecto de formalización Alexandria(enlace) del grupo de Paulson es impresionante
En especial, resulta interesante su trabajo sobre la formalización de algoritmos de computación cuántica(enlace al artículo)
Antes creía que los tipos dependientes eran el futuro, pero en proyectos reales la caída de productividad fue grande
Ahora prefiero soluciones claras y fáciles de mantener
Si el equipo puede entender y ampliar una herramienta, entonces esa es una buena herramienta
Me gustan más los sistemas de tipos que están en la frontera que los tipos dependientes completos
Por ejemplo, Purescript ofrece de forma nativa row-types más potentes que Haskell,
además de listas, cadenas y expresiones regulares a nivel de tipos
Eso se puede aprovechar con un enfoque de programación lógica basado en typeclasses