Measuring data types

Resumen Técnico: Midiendo Tipos de Datos

Planteamiento del Problema
Los lenguajes de programación funcional (por ejemplo, Haskell, Agda, Coq) dependen fuertemente de los tipos de datos inductivos, los cuales están categóricamente justificados como álgebras iniciales de endofuntores, específicamente endofutores polinómicos conocidos como tipos W. Si bien la semántica categórica de estos tipos está bien comprendida como álgebras iniciales, el artículo identifica una brece en la estructura matemática que los rodea. Específicamente, el marco categórico estándar trata los conjuntos-hom entre álgebras como meros conjuntos de homomorfismos totales. Esto no logra capturar las relaciones estructurales "parciales" o "aproximadas" entre tipos de datos, las cuales son cruciales para entender cómo los morfismos interactúan con las estructuras inductivas de una manera graduada o estratificada. Los autores buscan dilucidar la estructura en la que los tipos W están embebidos mediante el dibujo de una analogía con la teoría clásica de los coálgebras de medición de Sweedler, donde los álgebras sobre un cuerpo están enriquecidas en coálgebras.

Metodología
El artículo emplea una síntesis de dos teorías categóricas distintas:

1. Coálgebras de Medición de Sweedler: Los autores revisan la teoría clásica donde los $k$-álgebras están enriquecidas en $k$-coálgebras. En este entorno, el objeto-hom entre dos álgebras no es un conjunto de homomorfismos, sino una coálgebra de "homomorfismos parciales" (o mediciones). Estas mediciones permiten morfismos que son "casi" homomorfismos, donde la estructura de coálgebra codifica "qué tan cerca" está un morfismo de ser un homomorfismo total.
2. Tipos W y Tipos de Datos Inductivos: El artículo revisa la semántica categórica de los tipos inductivos como álgebras iniciales de endofutores (específicamente endofutores polinómicos).

La metodología central consiste en generalizar la teoría de Sweedler desde el contexto de álgebras sobre un cuerpo a álgebras de un endofutor arbitrario $F$ en una categoría monoidal cerrada simétrica $\mathcal{C}$. Los autores asumen que $\mathcal{C}$ es localmente presentable y que $F$ es un endofutor accesible y lax monoidal simétrico. Construyen un enriquecimiento de la categoría de $F$-álgebras ($\text{Alg}_F$) sobre la categoría de $F$-coálgebras ($\text{coAlg}_F$).

Pasos técnicos clave incluyen:

• Definir mediciones (mapas $C \otimes A \to B$) y homomorfismos parciales (mapas $C \to [A, B]$) para $F$-álgebras y $F$-coálgebras.
• Probar la existencia de una coálgebra de medición universal $\text{Alg}(A, B)$, que sirve como el objeto-hom en la categoría enriquecida.
• Construir el tensor de medición $C \triangleright A$ y el álgebra de convolución $[C, B]$ para establecer que la categoría es tensoreada y cotensoreada.
• Generalizar la noción de álgebras iniciales a álgebras $C$-iniciales, donde $C$ es una coálgebra, de forma análoga a los límites ponderados en la teoría de categorías enriquecidas.

Contribuciones Clave y Resultados

1. Enriquecimiento de Álgebras en Coálgebras (Teorema 10):
   El resultado central establece que para una categoría monoidal cerrada simétrica localmente presentable $\mathcal{C}$ y un endofutor lax monoidal simétrico accesible $F$, la categoría de $F$-álgebras está enriquecida, tensoreada y cotensoreada sobre la categoría de $F$-coálgebras.

   • En lugar de un conjunto de homomorfismos $\text{Alg}(A, B)$, existe una coálgebra $\text{Alg}(A, B)$ que representa todos los posibles homomorfismos parciales.
   • Este enriquecimiento se caracteriza por isomorfismos naturales:
     $$\text{coAlg}(C, \text{Alg}(A, B)) \cong \text{Alg}(C \triangleright A, B) \cong \text{Alg}(A, [C, B])$$

2. Generalización de los Tipos W:
   Los autores generalizan el concepto de tipos W (álgebras iniciales de endofutores polinómicos) a álgebras $C$-iniciales. Un álgebra $C$-inicial es un álgebra $A$ tal que para cualquier álgebra $X$, existe un único homomorfismo de coálgebra $C \to \text{Alg}(A, X)$. Esto permite una clasificación más matizada de los tipos inductivos basada en la "forma" o "profundidad" codificada por la coálgebra $C$.

3. Torre de Homomorfismos Parciales:
   El artículo construye una torre de coálgebras $\text{Alg}_n(A, B)$ que representa homomorfismos $n$-parciales. El límite de esta torre, $\text{Alg}_\infty(A, B)$, corresponde a homomorfismos $\infty$-parciales, que aproximan a los homomorfismos de álgebra totales. Esto proporciona un mecanismo formal para la "inducción parcial", donde uno puede construir inductivamente homomorfismos capa por capa.

4. Ejemplos Explícitos y Cálculos:
   La teoría se aplica a varios tipos de datos estándar en ciencias de la computación, incluyendo:

   • Tipos Unidad y Vacío: Demostrando enriquecimientos triviales.
   • Tipos Monoide: Mostrando cómo la estructura monoidal introduce "giros" (twists) en las mediciones.
   • Números Naturales: Calculando la coálgebra de medición universal para preálgebras iniciales (truncamientos finitos de $\mathbb{N}$) y probando que el truncamiento finito $n$ es el álgebra $n^\circ$-inicial terminal.
   • Listas y Árboles: Extendiendo la teoría a tipos de listas (sobre un monoide) y árboles binarios/generales. Los autores demuestran cómo las mediciones pueden controlar tanto la "forma" (profundidad/ramificación) como el "giro" (modificación elemento a elemento) de las estructuras de datos. Por ejemplo, muestran que mientras que un homomorfismo de álgebra total de una lista truncada al tipo de lista completa puede no existir, una medición sí lo hace.

Significancia y Reivindicaciones
El artículo afirma proporcionar la "forma más pura" del fenómeno de Sweedler al aplicarlo a endofutores, los cuales carecen de las restricciones de coherencia (unidades, multiplicación) de las álgebras tradicionales. Los autores argumentan que este enriquecimiento ofrece herramientas de mayor precisión para estudiar las interacciones entre álgebras, yendo más allá de la distinción binaria de "es un homomorfismo" o "no lo es".

La significancia es doble:

1. Matemáticas Puras: Unifica la teoría de las coálgebras de medición con la teoría de los tipos W, extendiendo el alcance de la teoría de Sweeder a un entorno categórico más amplio. Generaliza la noción de álgebras iniciales a álgebras $C$-iniciales, ofreciendo una nueva perspectiva sobre los tipos inductivos.
2. Teoría de Lenguajes de Programación: El marco proporciona una justificación categórica para las operaciones "parciales" sobre tipos inductivos. Los autores sugieren que esta estructura podría eventualmente informar la implementación de tipos inductivos en lenguajes de programación funcional (como Haskell), permitiendo potencialmente un manejo más flexible de datos parciales o flujos infinitos (streams).

El artículo señala explícitamente que es una versión extendida de un trabajo previo [20], añadiendo introducciones expositivas, pruebas completas y una construcción de torre generalizada para la inducción parcial. Reconoce que, si bien la teoría está establecida para endofutores específicos (como los de listas y árboles), la functorialidad de la construcción en la categoría $\mathcal{C}$ y el endofutor $F$ sigue siendo un tema de trabajo futuro. Del mismo modo, las implementaciones concretas en lenguajes de programación se identifican como una dirección futura más que como un resultado actual.