Constructing (Co)inductive Types via Large Sizes

Aquí se presenta un resumen técnico detallado del artículo "Constructing (Co)inductive Types via Large Sizes" de Bastiaan Laarakker, Daniël Otten y Benno van den Berg.

1. Enunciado del Problema

Los asistentes de prueba (por ejemplo, Agda, Lean, Rocq) dependen de la teoría de tipos dependientes para garantizar la consistencia y la decidibilidad. Un requisito crítico es que todas las funciones recursivas deben ser totales (terminantes) y todas las funciones corecursivas deben ser productivas.

• Limitaciones Actuales: La mayoría de los sistemas imponen la totalidad mediante comprobaciones sintácticas (por ejemplo, recursión estructural o terminación por cambio de tamaño). Estas comprobaciones suelen ser restrictivas, no modulares y sensibles a la refactorización del código.
• Tipos con Tamaño: Una alternativa basada en tipos utiliza "tamaños" (ordinales) para anotar los tipos, permitiendo demostrar la terminación mediante inducción bien fundada sobre el tamaño.
• La Inconsistencia de Agda: Agda implementa tipos con tamaño pero introduce un tamaño máximo ($\infty$) para definir el tipo inductivo/coinductivo completo como su aproximación en $\infty$. Esto conduce a una inconsistencia lógica: el sistema prueba $\infty < \infty$, violando la irreflexividad de los órdenes bien estrictos.
• Trabajo Teórico Previo: Los intentos anteriores de solucionar esto utilizando cuantificadores paramétricos (existencial $\exists$ para inductivo, universal $\forall$ para coinductivo) fueron limitados. Específicamente, solo podían construir tipos inductivos de ramificación finita porque el tipo de tamaño se interpretaba como el conjunto de números naturales ($\mathbb{N}$), el cual carece de ordinales límite necesarios para estructuras de ramificación infinita.

Objetivo: Construir una teoría de tipos consistente que soporte todos los tipos (co)inductivos (incluyendo los de ramificación infinita) utilizando tipos con tamaño y cuantificadores paramétricos, sin depender de un tamaño máximo inconsistente.

2. Metodología

Los autores extienden la Teoría de Tipos de Martin-Löf (MLTT) con características específicas para lograr esta construcción y probar su consistencia mediante un modelo de realizabilidad.

A. La Teoría de Tipos Extendida

La teoría incluye las características estándar de MLTT (universos, $\Sigma$, $\Pi$, tipos de identidad) más:

1. Un Tipo de Tamaños (Size):
   • Equipado con un cero ($0$) y un sucesor ($\uparrow i$).
   • Ordenado por un preorden ($\leq$) codificado como una mera proposición.
   • Crucialmente: Size es un tipo grande (no está en el universo $U$), pero la cuantificación sobre él puede producir tipos pequeños.
2. Cuantificadores Paramétricos:
   • $\exists i. A(i)$ (Existencial): Representa la unión de aproximaciones. Los términos son pares $\langle s, a \rangle$, pero el tamaño $s$ está abstraído (no se puede hacer pattern matching). La eliminación está restringida a tipos pequeños.
   • $\forall i. A(i)$ (Universal): Representa la intersección de aproximaciones. Las funciones actúan uniformemente sobre cualquier tamaño.
   • Axiomas de Parametricidad: La teoría incluye axiomas que establecen que estos cuantificadores conmutan con los constructores de tipos (por ejemplo, $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$). Esto internaliza la idea de que los tamaños se tratan uniformemente.
3. Inducción Bien Fundada (fix):
   • Un operador de punto fijo que permite la definición por inducción sobre tamaños: $fix\ f : \forall i. A(i)$ dado $f : \forall i. ((\forall j < i. A(j)) \to A(i))$.
   • La regla $\beta$ es proposicional (no definicional) para preservar la decidibilidad de la verificación de tipos.

B. Construcción de Tipos (Co)inductivos

Los autores codifican los tipos (co)inductivos como álgebras iniciales y coalgebras finales para endofuntores polinomiales ($F$).

1. Aproximaciones Ordinales: Definen funtores indexados por tamaño $F[\exists -]$ y $F[\forall -]$. Utilizando el operador fix, construyen álgebras iniciales ($\mu_3 F$) y coalgebras finales ($\nu_2 F$) para estos funtores indexados por tamaño. Estos representan el tipo truncado en un tamaño específico.
2. Tipos Completos mediante Cuantificación:
   • Tipos Inductivos: Definidos como $\mu F := \exists i. (\mu_3 F) i$. El cuantificador existencial recopila todos los términos acotados por algún tamaño.
   • Tipos Coinductivos: Definidos como $\nu F := \forall i. (\nu_2 F) i$. El cuantificador universal asegura que los términos sean observables a cualquier profundidad.
3. Manejo de Tipos de Ramificación Infinita: La innovación clave es demostrar que los funtores polinomiales conmutan débilmente con el cuantificador existencial. Esto requiere la existencia de ordinales límite (supremos de secuencias de tamaños), lo cual es imposible si los tamaños son simplemente $\mathbb{N}$.

C. Prueba de Consistencia: Modelo de Realizabilidad

Para probar que la teoría es consistente, los autores construyen un modelo de realizabilidad basado en el Topos Efectivo de Hyland.

• Interpretación de Tipos:
  • Tipos Pequeños: Interpretados como Relaciones de Equivalencia Parcial (PER) sobre números naturales (datos computables).
  • Tipos Grandes: Interpretados como Ensamblajes (conjuntos con relaciones de computabilidad).
• Interpretación de Size:
  • El tipo Size se interpreta como $\nabla \omega_1$, donde $\omega_1$ es el primer ordinal no numerable (el conjunto de todos los ordinales numerables).
  • Se le asigna la relación de realizabilidad "completa", lo que significa que los morfismos deben tratar todos los tamaños de manera uniforme (parametricidad).
• Validación:
  • Dado que $\omega_1$ contiene ordinales límite, el modelo valida los axiomas de parametricidad requeridos para tipos inductivos de ramificación infinita.
  • El modelo valida la Impredicatividad (cuantificar sobre tipos grandes produce tipos pequeños) y la Unicidad de las Pruebas de Identidad (UIP), aunque la sintaxis no asume estas propiedades. Esto demuestra que la sintaxis es compatible con teorías más fuertes (como la Teoría de Tipos de Homotopía) sin estar restringida por ellas.

3. Contribuciones Clave

1. Construcción General de Tipos (Co)inductivos: A diferencia de los enfoques paramétricos anteriores limitados a tipos de ramificación finita, este trabajo construye todos los tipos (co)inductivos, incluidos los de ramificación infinita (por ejemplo, ordinales de Brouwer, modelos de teoría de conjuntos constructiva).
2. Resolución de la Inconsistencia de Agda: Al reemplazar el inconsistente "tamaño máximo" ($\infty$) con cuantificadores paramétricos sobre un tipo grande de tamaños, los autores proporcionan una alternativa consistente a la implementación actual de Agda.
3. Cuantificadores Paramétricos como Mecanismo: Demuestran que internalizar la parametricidad mediante $\exists$ y $\forall$ sobre tamaños impone efectivamente la abstracción necesaria para prevenir comportamientos no terminantes e inconsistencias lógicas.
4. Modelo de Realizabilidad Robusto: La construcción de un modelo donde Size se interpreta como $\omega_1$ proporciona una justificación semántica rigurosa para la teoría, probando que los axiomas de parametricidad son consistentes.

4. Resultados

• Solidez Teórica: El artículo prueba que el álgebra inicial y la coalgebra final para cualquier endofunctor polinomial existen dentro de la teoría extendida.
• Consistencia: El modelo de realizabilidad confirma que la teoría es consistente. Muestra que los axiomas para cuantificadores paramétricos se cumplen cuando los tamaños se interpretan como un ordinal no numerable.
• Compatibilidad: Las construcciones no dependen de UIP o impredicatividad en la sintaxis, lo que hace que los resultados sean compatibles con la Teoría de Tipos de Homotopía (HoTT), a pesar de que el modelo satisface estas propiedades.

5. Significado y Trabajo Futuro

• Impacto en Asistentes de Prueba: Este trabajo ofrece un camino para implementar tipos con tamaño en asistentes de prueba (como Agda) sin la inconsistencia actual causada por el tamaño $\infty$. Permite una verificación de terminación más modular y composicional.
• Comportamiento Computacional: Los autores reconocen que, aunque la teoría es consistente, la sintaxis actual carece de comportamiento computacional para los axiomas de parametricidad (son axiomas, no reglas de reducción). El trabajo futuro debe conectar esto con la parametricidad interna (por ejemplo, mediante tipos puente o teoría de tipos cúbicos) para garantizar la decidibilidad y la canonicidad en la práctica.
• Decidibilidad de la Desigualdad: El modelo implica que la desigualdad en tamaños no es generalmente decidible (debido a los supremos). Los autores sugieren un enfoque híbrido (desigualdad definicional vs. proposicional) para la implementación práctica.
• Generalización: El modelo podría potencialmente generalizarse a otras álgebras de combinadores parciales o integrarse con efectos y univalencia.

En resumen, el artículo cierra exitosamente la brecha entre la necesidad teórica de tipos con tamaño paramétricos y el requisito práctico de consistencia, permitiendo la construcción de tipos (co)inductivos complejos en un marco de teoría de tipos sólido.