Revertible Effects: reversión de efectos en la dimensión temporal

论文版本948a07b (main)

El artículo usa Revertible Effects para resolver la temporal composability — cuando un componente se elimina, toda modificación que haya hecho al entorno debe revertirse completa y seguramente. Idea central: cada effect debe llevar un inverse (operación inversa), el runtime compone todos los inverses en un único acumulador y, al descargar, se aplican en orden LIFO.

El tipo de un Effect

[Conclusión original del artículo §3.1] El artículo modela un effect con el tipo Γ → Γ × (Γ → Γ): actúa sobre el contexto actual y devuelve el contexto modificado junto con una función inverse. El effect context se define como ∂Γ ≔ Γ × (Γ → Γ), donde la primera componente es el estado actual y la segunda es el acumulador — es decir, "el compuesto de los inverses de todos los effects hasta ahora", una función que restaura el contexto a su estado inicial.

El artículo §3.1.1 Def 3 da trackΓ: mapea (f, g) a ∂Γ → ∂Γ, produciendo para el estado (γ, φ) el valor (f(γ), φ ∘ g) — aplica f hacia adelante y compone el inverse g en el acumulador. Thm 7 prueba que recover(track(f,g)(γ,φ)) = recover(γ,φ), es decir, "recuperar tras rastrear es equivalente a recuperar directamente sin rastrear".

[Conclusión original del artículo §3.1.2] El artículo refuerza el modelo para que el inverse lo proporcione el llamador en el punto de aplicación del effect, según el estado actual (𝔈Γ ≔ Γ → Γ × (Γ → Γ)), y exige la condición witness g(δ) = γ (Def 8) — es decir, aplicar el inverse al estado post-effect debe restaurar el estado pre-effect. Múltiples effects se componen mediante ⋄ (Def 9), track es un monoid homomorphism (Thm 5), y la recuperación es exacta bajo orden LIFO (Thm 15, Thm 16).

ctx.effect: la correspondencia en la API de Cordis

Corresponde a ctx.effect de Cordis §5.1.1; pseudocódigo TypeScript:

ctx.effect(() => {
  const resource = acquire()
  return () => {
    release(resource)
  }
})

ctx.effect toma una función que ejecuta el effect hacia adelante (adquirir un recurso) y devuelve una función cleanup (liberar el recurso). El runtime compone el cleanup en el acumulador del contexto padre.

• Composición de múltiples inverses: dispose se antepone al ctx.dispose del contexto padre, de modo que el inverse del effect hijo es en realidad un effect sobre el padre (corresponde a la estructura recursiva de ∂²Γ). El desarrollador solo escribe inverses para effects atómicos; el inverse compuesto se deriva automáticamente vía ⋄.
• Orden LIFO: el inverse ← value ∘ inverse del Algorithm 1 compone el nuevo inverse al frente, y al descargar se aplican en orden inverso. Los effects registrados más tarde se revertir primero, en consonancia con la intuición "last-in-first-out" del ciclo de vida de los recursos.
• Comparación con React useEffect cleanup, RAII y rollback de transacciones: [Conclusión original del artículo §7.3] React useEffect empareja effect con cleanup estructuralmente, pero los hooks no pueden llamarse en condiciones/bucles/funciones anidadas, el cuerpo del effect no admite funciones async ni iteradores, y no se puede componer un inverse compuesto a partir de effects existentes; RAII / tipos lineales confinan la reversal a una región léxica; STM confina el rollback al interior de la transacción; los effects de Cordis son operaciones ordinarias, libremente composables, pueden ser async, y solo exigen escribir inverses para cada effect atómico — el inverse compuesto se deriva automáticamente por composición.

ctx.effect no verifica la corrección del inverse

[Conclusión original del artículo §3.1.3] ctx.effect solo rastrea inverses; no prueba automáticamente que un inverse sea correcto. La condición witness g(δ) = γ es una obligación del desarrollador, no una verificación del runtime. Si un inverse está mal escrito (p. ej. libera el recurso equivocado, o sus efectos secundarios son asimétricos respecto del effect), la recuperación fallará o contaminará el estado, y el runtime no se responsabiliza.

Independence (Def 19) exige que los monoids de transformación de dos effects conmuten entre sí y que no perturben el inverse del otro — esta es la precondition para generalizar el LIFO de un único componente a secuencias intercaladas de múltiples componentes (Cor 21). Los effects no conmutativos (p. ej. una cadena ordenada de operaciones) necesitan ordenamiento vía coeffects para garantizar la recoverability.

Núcleo de esta sección

Concepto teórico	Implementación en Cordis
Unified Context Γ∞	ctx, contexto de primera clase
Revertible Effect	ctx.effect(callback)
Inverse Accumulator	fiber.dispose
Condición witness g(δ)=γ	Obligación del desarrollador, el runtime no verifica
Composición LIFO ⋄	track es un monoid homomorphism (Thm 5)

Los Revertible Effects resuelven "revertir", pero los componentes también deben "responder a cambios de dependencias". Esto último lo resuelven los Reactive Coeffects.