Ciclo de vida del componente y orden de descarga

论文版本948a07b (main)

Los Revertible Effects resuelven "revertir"; los Reactive Coeffects resuelven "percibir cambios de dependencia". Para que ambos se coordinen sobre una instancia de componente se necesita una máquina de estados completa de ciclo de vida. El artículo §4.3 da este mecanismo, y el orden de descarga de Provider/Consumer es el detalle de ingeniería más importante.

Máquina de estados completa

[Conclusión original del artículo §4.3 Def 49] La máquina de estados completa del ciclo de vida de un componente (fiber):

Las siete primitivas L-:

Primitiva	Disparador	Semántica
L-Begin	target ≠ ⊥ y el fiber está en Inactive	Entra en Reloading, registra committed view, arranca el effect iterator
L-Iter	En Reloading, target = ω, el iterator produce Just(i')	Aplica el effect de una iteration, compone el inverse en el acumulador
L-Finish	En Reloading, el iterator produce Nothing	Todos los effects instalados, entra en Active
L-Divert	En Reloading, target ≠ ω (dependencia cambiada)	Aborta/aterriza la iteration actual, entra en Unloading (ya sea abort, o land y luego unload)
L-Raise	La iteration lanza un error ξ	Entra en Unloading llevando ξ; el L-Unload subsiguiente aplica el acumulador existente
L-Leave	En Active, target ≠ ω	Marca Unloading pero no aplica inverse; deja de proveer coeffect
L-Unload	En Unloading, ¬ relied_n(γ)	Aplica el acumulador g, entra en Inactive

Orden de descarga de Provider y Consumer

[Conclusión original del artículo §4.3.1] Este es uno de los mecanismos de ingeniería más importantes del artículo. El L-Unload del cálculo base pone "eliminar provision" y "ejecutar inverse" juntos, sin dejar intervalo para el teardown del consumer. Si el provider aplica inverse directamente para liberar recursos mientras un consumer aún usa la dependencia del provider, aparecen caídas como "el pool de conexiones de la base de datos se cerró mientras una transacción no se había comprometido todavía".

El artículo introduce un estado intermedio Unloading y un guard ¬ relied_n(γ) (ningún fiber depende ya de n) para garantizar el orden correcto:

1. L-Leave: el Provider n marca Unloading, deja de proveer coeffect (su σ sale del union de σ_γ), pero conserva intactos su propio committed view e inverse;
2. El Consumer m detecta que su dependencia está a punto de desaparecer (target view se vuelve ⊥ o apunta a otro fiber);
3. El Consumer m usa la dependencia vieja de su committed view para terminar la limpieza — porque σ_γ solo hace union de fibers Active, el binding de un fiber Unloading es invisible para otros fibers, pero el committed view del consumer aún apunta a él;
4. L-Unload se ejecuta cuando el guard ¬ relied_n(γ) se satisface — es decir, todos los consumers que dependen de n se han desactivado;
5. El Provider n recién entonces ejecuta su propio inverse y libera recursos.

Este mecanismo resuelve:

• Esperar a que las conexiones se devuelvan antes de cerrar el pool
• Esperar a que las transacciones se comprometan antes de cerrar la base de datos
• Esperar a los Agentes que están usando un Tool Provider antes de descargarlo
• Limpieza en cascada de componentes hijos cuando el padre sale

[Conclusión original del artículo §4.4.4 Thm 66] El guard no puede entrar en deadlock: σ_γ solo hace union de fibers Active; una vez L-Leave marca a n, su tabla sale de σ_γ, ningún target view puede ya apuntar a n, y todos los consumers comprometidos con n se ven forzados a su propio teardown; el grafo de dependencias se propaga hacia abajo por la relación ≺, y la aciclicidad + finitud garantiza la liberación del guard (véase el teorema de Progress).

Inertia: ¿qué pasa si la dependencia cambia durante la carga asíncrona?

[Conclusión original del artículo §4.3.3] Los effects modernos suelen ser asíncronos (fetch, IO de ficheros, llamadas a sub-Agentes). Una vez que una iteration está en vuelo (un async Future), debe aterrizar, no se puede abortar. Si target view cambia durante el vuelo, L-Divert solo puede elegir la rama "aterrizar y luego unload"; no puede "abortar la iteration" — porque una vez que una iteration se ha comprometido a un Future, no se puede cancelar.

Tres conceptos relacionados:

• Inertia: el handle de la transición en vuelo, no cancelable, solo se puede esperar a que aterrice;
• Iteration boundary: la granularidad a la que L-Divert interviene — el cambio de target solo se comprueba en los límites de iteration;
• Partial rollback: el inverse acumulado se aplica, la parte inacabada se revierte;
• Recarga y descarga enlazadas: al completar reload, si el target ya cambió, encadena con unload; al completar unload, si el target ya cambió, encadena con reload (Algorithm 5).

Este mecanismo garantiza que al cargar componentes de forma asíncrona nunca se llega a "medio viejo, medio nuevo" — o termina entrando en Active, o entra en Unloading vía L-Divert/L-Raise y se revierte por completo (corresponde al teorema de Resolution Coherence).

Correspondencia teoría→implementación

[Conclusión original del artículo §5.1 Table 2] Correspondencia entre los conceptos formales del artículo y la implementación de Cordis:

Concepto teórico	Implementación en Cordis
Unified Context Γ∞	ctx, contexto de primera clase
Revertible Effect	ctx.effect(callback)
Registro y acceso de coeffect	ctx.set(key, value) / ctx.get(key)
Component Instantiation	ctx.use(component, config)
Dependency Specification	fiber.inject (el d teórico)
Inverse Accumulator	fiber.dispose
Committed View	fiber.committed
Target View	fiber.target (recalculado por refresh)
Isolation	ctx.isolate(key, realm)
Interception	ctx.intercept(key, metadata)
Inertia	fiber.inertia (handle de transición en vuelo)
Lifecycle State	fiber.state (LOADING=Reloading, FAILED=Inactive(ξ))

Diferencia entre Fiber y React Fiber

[Inferencia basada en el artículo] La Def 44 del artículo define un fiber como una instanciación de un componente, portando (d, p, e, π, σ, τ, θ) — fiber padre, tabla de coeffect propia, marcador de retirement, estado de ciclo de vida. Comparte solo el nombre con React Fiber, no el concepto: React Fiber es la unidad interna de reconciliation de React, portadora del estado de recorrido del árbol de componentes; Cordis Fiber es una instancia de componente en el cálculo de composición dinámica, portadora del accumulator de effects, committed view y máquina de estados del ciclo de vida. Ambos toman prestado el sentido de "hilo de ejecución ligero" de la palabra "fiber", pero los marcos teóricos son completamente distintos.

A continuación, lo que este mecanismo garantiza a nivel metateórico: Traducción de ingeniería de los teoremas formales.