Type Theory With Erasure

1. Planteamiento del Problema

En los lenguajes de programación con tipos dependientes (como Agda, Idris y Rocq), los tipos a menudo dependen de valores. Esto crea una ambigüedad fundamental: ¿qué partes de un programa son computacionalmente relevantes en tiempo de ejecución y cuáles pueden ser eliminadas de forma segura durante la compilación?

• Enfoques Actuales: Las soluciones existentes suelen depender de la Teoría de Tipos Cuantitativa (QTT), que utiliza un semianillo cuantitativo (por ejemplo, $\{0 < \omega\}$) para rastrear el uso de variables. Aunque es efectiva, la QTT introduce complejidad en cuanto a restricciones subestructurales y linealidad. Otros enfoques utilizan "clases fantasma" o análisis heurístico de todo el programa, lo cual puede ser frágil e impredecible para tipos dependientes complejos.
• La Brecha: Existe la necesidad de una formulación estructural, modular y libre de reducción de la eliminación que se integre perfectamente con la metateoría estándar de la teoría de tipos, soporte la extracción de código y proporcione una base semántica clara sin depender de semánticas cuantitativas complejas.

2. Metodología

Los autores proponen una versión estructural de la teoría de tipos con eliminación formulada como una Teoría Algebraica Generalizada de Segundo Orden (SOGAT).

• Distinción de Fase Sintética: En lugar de utilizar semianillos cuantitativos, los autores codifican la eliminación como una distinción de fase utilizando una proposición sintética, denotada como # (el marcador de eliminación).
  • Un contexto $\Gamma$ se considera "eliminado" si contiene la proposición $\#$ (es decir, $\# \in \Gamma$).
  • Esto crea una distinción entre el modo de ejecución ($\omega$) y el modo eliminado ($0$).
  • Crucialmente, $\#$ es una proposición sin valor de verdad; no puede ser construida ni descargada arbitrariamente. Actúa como un marcador que permite coaccionar términos entre modos.
• Mecanismo de Coacción: La teoría introduce dos coacciones:
  • Eliminación ($\#$): Si un término $a$ es de tipo $A$ en un contexto extendido por $\#$, puede ser coaccionado a un término eliminado ($\# a : 0: A$).
  • Levantamiento (\$): Si un término $a$ está eliminado, puede ser levantado a un término de ejecución bajo la suposición de $\#$ (\ a : \omega: A$).
  • Estas son inversas mutuas hasta la igualdad definicional, asegurando que los términos eliminados no dependan de datos de ejecución.
• Formulación Modular SOGAT: La teoría se define como una SOGAT que extiende la Teoría de Tipos de Martin-Löf (MLTT). Esto permite a los autores aprovechar la metateoría existente para las SOGATs, incluyendo semántica functorial y construcción de modelos mediante Categorías con Familias (CwFs).

3. Contribuciones Clave

A. Formulación Teórica

• Definición SOGAT: El artículo define TT0 (Teoría de Tipos con Eliminación) como una SOGAT. Incluye tipos ($Ty$), términos ($Tm$) indexados por modos $\{0, \omega\}$, y el marcador de eliminación ($\#$).
• Fragmento Eliminado Derivado: Una contribución significativa es que la teoría no necesita definir explícitamente versiones eliminadas de cada formador de términos (por ejemplo, $\Pi_0, \Sigma_0$). Debido al isomorfismo entre contextos con y sin $\#$, todo el fragmento eliminado se deriva automáticamente del fragmento de ejecución.
• Tipos Inductivos: El marco soporta tipos inductivos donde argumentos específicos (como índices) pueden marcarse como eliminados. Maneja tipos inductivos "exóticos" donde los propios constructores podrían existir solo en modo eliminado.

B. Modelos Semánticos

• Modelo Fam(Set): Los autores construyen un modelo estándar en la categoría de familias de conjuntos ($Fam(Set)$).
  • En este modelo, un objeto es un par $(X_0, X_1)$ donde $X_0$ representa datos eliminados y $X_1$ representa datos de ejecución.
  • El marcador de eliminación $\#$ se interpreta como una "pequeña proposición" (un objeto $\phi$ tal que la exponenciación por $\phi$ aísla el componente base).
  • Este modelo se generaliza a cualquier topos de Grothendieck equipado con una pequeña proposición.
• Universos Aplastados: Para manejar universos en el contexto eliminado, los autores introducen "universos aplastados" ($\sqrt{\phi}U$). Estos son objetos modales $\phi$ que retienen la estructura de los universos estándar pero satisfacen la condición de que sus fibras son contractibles, permitiéndoles existir en contextos eliminados sin portar datos de ejecución.

C. Extracción de Código y Corrección

• Extracción a Cálculo Lambda No Tipado: Los autores construyen un modelo que extrae programas TT0 al cálculo lambda no tipado.
  • Los términos de ejecución se mapean a términos lambda.
  • Los términos eliminados se mapean al objeto terminal (desapareciendo efectivamente).
  • Los contextos con variables eliminadas son isomorfos a contextos sin ellas.
• Pegado y Relaciones Lógicas: Para probar la corrección, utilizan pegado para construir una relación lógica entre el modelo de extracción de código y el modelo estándar de teoría de conjuntos.
  • Teorema 27 (No interferencia): Prueba que toda función eliminada es constante en tiempo de ejecución. Si una función toma un argumento eliminado, su salida no puede depender de ese argumento en tiempo de ejecución.
  • Teoremas 25 y 26: Prueban la canonicidad y que el código extraído rastrea la interpretación semántica.

D. Implementación

• Elaborador: Se implementó un elaborador de juguete en Agda. Toma un lenguaje de alto nivel (similar a Idris/Agda con anotaciones 0 y @0) y lo elabora en la SOGAT central.
• Unificación de Patrones: Los autores demuestran que, dado que el núcleo es estructural, los algoritmos estándar de unificación de patrones pueden reutilizarse sin necesidad de verificaciones de cantidad complejas o mecanismos de generalización especiales para metavariables eliminadas, resolviendo problemas encontrados en las implementaciones actuales de Agda e Idris.

4. Resultados

• Conservatividad: Se ha demostrado que la teoría es conservativa sobre MLTT. Añadir eliminación no aumenta el poder demostrativo de la teoría de tipos; cualquier teorema demostrable en TT0 es demostrable en MLTT estándar.
• Independencia: Se ha demostrado que los datos eliminados son independientes de los datos de ejecución. Un término eliminado en un contexto $\Gamma$ corresponde de manera única a un término eliminado en el contexto "cero" $0\Gamma$ (donde todos los modos se establecen en 0).
• Corrección de la Extracción: La prueba de pegado confirma que el proceso de extracción preserva el comportamiento computacional y elimina correctamente los datos irrelevantes, asegurando que el código generado sea seguro y eficiente.

5. Significado

• Claridad Estructural: Al alejarse de los semianillos cuantitativos hacia una distinción de fase sintética, el artículo proporciona una base más limpia y modular para la eliminación. Separa el concepto de eliminación del mecanismo de rastreo de recursos.
• Guía de Implementación: El enfoque estructural simplifica la implementación de verificadores de tipos y elaboradores. Elimina la necesidad de verificaciones de cantidad ad hoc durante la unificación, potencialmente corrigiendo errores en sistemas existentes como Idris 2 y Agda.
• Base Semántica: El uso de topos de Grothendieck y pequeñas proposiciones conecta la eliminación con la lógica categórica más amplia, permitiendo el uso de la Computabilidad Sintética de Tait para pruebas metateóricas.
• Extensiones Futuras: El marco está diseñado para ser extensible, apoyando trabajos futuros potenciales sobre tipos en tiempo de ejecución, múltiples distinciones de fase (para etapas/metaprogramación) e integración con la Teoría de Tipos Cúbica.

En resumen, este artículo presenta un enfoque riguroso, estructural y semánticamente fundamentado para la teoría de tipos con eliminación, ofreciendo tanto garantías teóricas (conservatividad, no interferencia) como beneficios prácticos para la implementación de compiladores y la extracción de código.