You may implement this later: Cofunctors as partial implementations

Resumen Técnico: Cofuntores como Implementaciones Parciales

Planteamiento del Problema
En la programación funcional y la ingeniería de software, el modelo estándar de implementación es el functor: un mapeo de una categoría de especificación ($S$) a una categoría de implementación concreta ($C$) donde cada objeto y morfismo de la especificación se asigna inmediatamente a una instancia concreta. Sin embargo, el desarrollo de software en el mundo real a menudo requiere una configuración por etapas, donde las elecciones de implementación (por ejemplo, representaciones de datos, algoritmos, protocolos de backend) se difieren en el tiempo.

Los enfoques actuales, como los módulos parametrizados (funtores de ML), dependen de un único tipo de parámetro global ($P$) suministrado de antemano ($S \times P \to C$). Este modelo falla cuando las elecciones de implementación son dependientes del estado: una elección realizada en una etapa (por ejemplo, seleccionar un backend de persistencia) puede introducir nuevas obligaciones o restricciones en una etapa posterior (por ejemplo, requerir un formato de serialización específico o un protocolo de transacciones). El desafío consiste en modelar sistemas donde el conjunto de opciones de implementación disponibles evoluciona dinámicamente a medida que la especificación evoluciona, sin necesidad de enumerar todas las configuraciones finales posibles de antemano.

Metodología
El artículo propone modelar las implementaciones parciales utilizando cofuntores (también conocidos como retrofuntores). La metodología consiste en construir una categoría de implementaciones parciales ($P$) basada en una categoría de especificación ($S$) y un funtor de elecciones ($Choice: S \to \mathbf{Set}$).

1. Elecciones Dependientes del Estado: Para cada objeto de especificación $A$, existe un conjunto de estados de elección $Choice(A)$. Estos estados representan configuraciones parciales donde algunos campos están fijados y otros están abiertos (obligaciones).
2. Transporte de Elecciones: Los morfismos de especificación $f: A \to B$ inducen una función de "transporte" $f^*: Choice(A) \to Choice(B)$. Esta función actualiza el estado de la implementación llevando adelante las elecciones existentes e introduciendo nuevas obligaciones o conflictos basados en el cambio de la especificación.
3. La Estructura del Cofuntor: Un cofunctor se define como un span $S \xleftarrow{p} \Lambda \xrightarrow{q} P$ donde:
   • $q$ es biyectivo en objetos (identificando los objetos de $P$ con pares $(A, c)$ donde $A \in S$ y $c \in Choice(A)$).
   • $p$ es una opfibración discreta, que codifica el menú dependiente de elecciones.
   • El mapa de morfismo, impl, toma un cambio de especificación $f$ y una elección actual $c$ para producir un morfismo de implementación. Crucialmente, el objetivo de este morfismo depende de la elección transportada $f^*c$.
4. Leyes de Composición: La implementación de un cambio de especificación compuesto $g \circ f$ se define implementando $f$ con la elección $c$, actualizando el estado a $f^*c$, y luego implementando $g$ con el nuevo estado. Esto asegura que el orden de las operaciones respete la evolución de las obligaciones.

El artículo demuestra esto mediante una implementación en Idris, utilizando tipos dependientes para asegurar que el estado de la implementación (la elección) se actualice y rastree correctamente a través de cada transición de la especificación.

Contribuciones Clave

• Lectura Conceptual: La contribución principal es la novedosa interpretación de los cofuntores como implementaciones parciales. Aunque los cofuntores (o retrofuntores) existen en la teoría de categorías (por ejemplo, en el contexto de lentes delta o categorías internas), este artículo los enmarca explícitamente como un mecanismo para gestionar elecciones de implementación parciales y dependientes del estado.
• Gestión Dinámica de Obligaciones: A diferencia de la parametrización estática, este enfoque permite que el "menú" de elecciones de implementación cambie dinámicamente. Soporta escenarios donde una etapa posterior (por ejemplo, la replicación) puede introducir nuevos requisitos (por ejemplo, registros de transacciones) que no estaban presentes en etapas anteriores (por ejemplo, almacenamiento simple), y puede detectar conflictos (por ejemplo, un backend no transaccional fallando un requisito de replicación) sin definir previamente todas las combinaciones posibles.
• Planes de Migración Ejecutables: El marco permite la construcción de planes de migración ejecutables que componen pasos de implementación. Distingue entre transportes (cambios impulsados por la evolución de la especificación) y refinamientos (llenar los huecos en el estado de elección sin cambiar la especificación).
• Comparación con Alternativas: El artículo argumenta que, si bien herramientas como Backpack (para el enlace de mixins estáticos) o las codificaciones tagless-final (para diferir intérpretes) resuelven problemas relacionados, no soportan nativamente la transformación indexada por estado de sistemas en ejecución donde las obligaciones se resuelven de forma incremental y composicional.

Resultos y Ejemplos
El artículo proporciona un ejemplo concreto de un sistema de almacenamiento que evoluciona de un Store genérico a un PersistentStore y finalmente a un ReplicatedStore.

• Escenario: Partiendo de un estado de elección que contiene un backend SQLite pero con un serialiser y un cache indefinidos.
• Proceso:
  1. Persist (Persistir): Transporta el estado, preservando el backend pero registrando una obligación de durabilidad.
  2. Replicate (Replicar): Transporta el estado nuevamente. Si el backend es SQLite, tiene éxito al introducir una obligación de protocol. Si el backend es un FlatFile no transaccional, el transporte resulta explícitamente en un estado de Conflict (Conflicto).
• Resultado: El sistema genera un plan de migración tipado que compone estos pasos. El plan puede ejecutarse para producir un sistema concreto (por ejemplo, SQLite/CBOR/LRU/Raft) o ser rechazado si surgen conflictos. La ley de composición asegura que un plan de una sola pasada para "Persistir y Replicar" es equivalente a la ejecución por etapas de "Persistir" y luego "Replicar".

Significancia y Reivindicaciones
El artículo afirma modestamente que los ingredientes (cofuntores, configuración por etapas, tipos dependientes) no son nuevos. Su contribución específica es la lectura conceptual que conecta estas estructuras categóricas con el problema práctico de la implementación parcial en la programación funcional.

El autor sostiene que el eslogan "los cofuntores son implementaciones parciales" es una nueva visión desmitificadora. Esta lectura proporciona una base formal para:

1. Gestionar implementaciones parciales compuestas donde las elecciones dependen del estado actual de la especificación.
2. Separar el entorno de gestión de obligaciones (el cofuntor) de la semántica final (el funtor hacia la categoría concreta).
3. de Manejar la migración y configuración dinámica en sistemas donde el conjunto de elecciones de implementación válidas no es estático, sino que evoluciona con la arquitectura del sistema.

El artículo concluye que, si bien los cofuntores se han utilizado en la teoría de categorías monoidales y en la propagación de actualizaciones de bases de datos (lentes), su aplicación como una herramienta independiente para gestionar elecciones de implementación dependientes del estado en la programación funcional ha sido previamente pasada por alto, probablemente debido a la confusión terminológica con los functores contravariantes y al predominio de las perspectivas de bases de datos en la literatura de lentes.