Revertible Effects : réversion des effets de bord temporels

论文版本948a07b (main)

L'article utilise les Revertible Effects pour résoudre la temporal composability — lorsqu'un composant est retiré, toute modification qu'il a faite à l'environnement doit être complètement et sûrement révertie. Idée centrale : tout effect doit porter un inverse (l'opération inverse), le runtime compose tous les inverses dans un accumulateur unique, et au déchargement ils sont appliqués en ordre LIFO.

Le type d'un Effect

[Conclusion originale de l'article §3.1] L'article modélise un effect par le type Γ → Γ × (Γ → Γ) : il agit sur le contexte courant et renvoie le contexte modifié ainsi qu'une fonction inverse. Le effect context est défini comme ∂Γ ≔ Γ × (Γ → Γ), où la première composante est l'état courant et la seconde est l'accumulateur — c.-à-d. « le composé des inverses de tous les effects jusqu'ici », une fonction qui restaure le contexte à son état initial.

L'article §3.1.1 Def 3 donne trackΓ : il mappe (f, g) vers ∂Γ → ∂Γ, produisant pour l'état (γ, φ) la valeur (f(γ), φ ∘ g) — applique f vers l'avant et compose l'inverse g dans l'accumulateur. Thm 7 prouve que recover(track(f,g)(γ,φ)) = recover(γ,φ), c.-à-d. que « récupérer après tracking équivaut à récupérer directement sans tracking ».

[Conclusion originale de l'article §3.1.2] L'article renforce le modèle afin que l'inverse soit fourni par l'appelant au point d'application de l'effect, en fonction de l'état courant (𝔈Γ ≔ Γ → Γ × (Γ → Γ)), et exige la condition witness g(δ) = γ (Def 8) — c.-à-d. appliquer l'inverse à l'état post-effect doit restaurer l'état pré-effect. Plusieurs effects se composent via ⋄ (Def 9), track est un monoid homomorphism (Thm 5), et la récupération est exacte sous l'ordre LIFO (Thm 15, Thm 16).

ctx.effect : la correspondance dans l'API Cordis

Cela correspond à ctx.effect de Cordis §5.1.1 ; pseudocode TypeScript :

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

ctx.effect prend une fonction qui exécute l'effect vers l'avant (acquérir une ressource) et renvoie une fonction cleanup (libérer la ressource). Le runtime compose le cleanup sur l'accumulateur du contexte parent.

• Composition de plusieurs inverses : dispose est prepend au ctx.dispose du contexte parent, de sorte que l'inverse de l'effect enfant est en réalité un effect sur le parent (correspondant à la structure récursive de ∂²Γ). Les développeurs n'écrivent des inverses que pour les effects atomiques ; l'inverse composite est dérivé automatiquement via ⋄.
• Ordre LIFO : le inverse ← value ∘ inverse de l'Algorithm 1 compose le nouvel inverse au début, et au déchargement les inverses sont appliqués en ordre inverse. Les effects enregistrés plus tard sont révertis en premier, ce qui correspond à l'intuition « dernier entré, premier sorti » du cycle de vie des ressources.
• Comparaison avec React useEffect cleanup, RAII et rollback de transaction : [Conclusion originale de l'article §7.3] React useEffect appareille structurellement effect avec cleanup, mais les hooks ne peuvent être appelés dans des conditions/boucles/fonctions imbriquées, le corps de l'effect n'accepte pas de fonctions async ou d'itérateurs, et un inverse composite ne peut être composé à partir d'effects existants ; RAII / types linéaires confinent la reversal à une région lexicale ; STM confine le rollback à l'intérieur de la transaction ; les effects de Cordis sont des opérations ordinaires, librement composables, peuvent être async, et ne requirent d'écrire un inverse que pour chaque effect atomique — l'inverse composite est dérivé automatiquement par composition.

ctx.effect ne vérifie pas la correction de l'inverse

[Conclusion originale de l'article §3.1.3] ctx.effect se contente de suivre les inverses ; il ne prouve pas automatiquement qu'un inverse est correct. La condition witness g(δ) = γ est une obligation du développeur, pas une vérification du runtime. Si un inverse est mal écrit (p. ex. libère la mauvaise ressource, ou ses effets de bord sont asymétriques par rapport à l'effect), la récupération échouera ou polluera l'état, et le runtime n'est pas responsable.

L'indépendance (Def 19) exige que les monoids de transformation de deux effects commutent entre eux et ne perturbent pas l'inverse de l'autre — c'est la précondition pour généraliser le LIFO d'un seul composant à des séquences entrelacées de plusieurs composants (Cor 21). Les effects non commutatifs (p. ex. une chaîne ordonnée d'opérations) nécessitent un ordonnancement par coeffect pour garantir la recoverability.

Cœur de cette section

Concept théorique	Implémentation Cordis
Unified Context Γ∞	ctx, contexte de première classe
Revertible Effect	ctx.effect(callback)
Inverse Accumulator	fiber.dispose
Condition witness g(δ)=γ	Obligation du développeur, non vérifiée par le runtime
Composition LIFO ⋄	track est un monoid homomorphism (Thm 5)

Les Revertible Effects résolvent « réverter » — mais les composants doivent aussi « répondre aux changements de dépendances ». Ce dernier point est résolu par les Reactive Coeffects.