Revertible Effects: zeitdimensionaler Seiteneffekt-Rollback

论文版本948a07b (main)

Das Papier verwendet Revertible Effects, um die temporal composability zu lösen — wenn eine Komponente entfernt wird, muss jede Änderung, die sie an der Umgebung vorgenommen hat, vollständig und sicher rückgängig gemacht werden. Kernidee: jeder Effect muss einen Inverse (die Umkehroperation) mit sich führen, die Laufzeit komponiert alle Inverses in einen einzigen Akkumulator, und beim Entladen werden sie in LIFO-Reihenfolge angewendet.

Der Typ eines Effects

[Originale Schlussfolgerung des Papiers §3.1] Das Papier modelliert einen Effect als Typ Γ → Γ × (Γ → Γ): er wirkt auf den aktuellen Kontext und gibt den modifizierten Kontext zusammen mit einer Inverse-Funktion zurück. Der Effect-Kontext wird als ∂Γ ≔ Γ × (Γ → Γ) definiert, wobei die erste Komponente der aktuelle Zustand ist und die zweite der Akkumulator — also „die Komposition der Inverses aller bisherigen Effects", eine Funktion, die den Kontext in seinen Ausgangszustand zurückversetzt.

Das Papier §3.1.1 Def 3 gibt trackΓ an: bildet (f, g) auf ∂Γ → ∂Γ ab und erzeugt für den Zustand (γ, φ) den Wert (f(γ), φ ∘ g) — wendet f vorwärts an und komponiert den Inverse g in den Akkumulator. Thm 7 beweist, dass recover(track(f,g)(γ,φ)) = recover(γ,φ), also „Recover nach Tracking ist äquivalent zu direktem Recover ohne Tracking".

[Originale Schlussfolgerung des Papiers §3.1.2] Das Papier verstärkt das Modell, sodass der Inverse vom Aufrufer am Anwendungspunkt des Effects aufgrund des aktuellen Zustands geliefert wird (𝔈Γ ≔ Γ → Γ × (Γ → Γ)), und verlangt die Witness-Bedingung g(δ) = γ (Def 8) — also: Anwenden des Inverse auf den Post-Effect-Zustand muss den Pre-Effect-Zustand wiederherstellen. Mehrere Effects komponieren sich über ⋄ (Def 9), track ist ein Monoid-Homomorphismus (Thm 5), und Recovery ist unter LIFO-Reihenfolge exakt (Thm 15, Thm 16).

ctx.effect: die Cordis-API-Entsprechung

Entspricht ctx.effect aus Cordis §5.1.1; TypeScript-Pseudocode:

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

ctx.effect nimmt eine Funktion, die den Vorwärts-Effect ausführt (Ressource akquirieren) und eine Cleanup-Funktion (Ressource freigeben) zurückgibt. Die Laufzeit komponiert das Cleanup auf den Akkumulator des Elternkontexts.

• Komposition mehrerer Inverses: dispose wird dem ctx.dispose des Elternkontexts vorangestellt, sodass der Inverse des Kind-Effects tatsächlich ein Effect auf dem Parent ist (entspricht der rekursiven Struktur von ∂²Γ). Entwickler schreiben nur Inverses für atomare Effects; der zusammengesetzte Inverse wird über ⋄ automatisch abgeleitet.
• LIFO-Reihenfolge: Algorithm 1's inverse ← value ∘ inverse komponiert den neuen Inverse vorne, und beim Entladen werden die Inverses in umgekehrter Reihenfolge angewendet. Später registrierte Effects werden zuerst rückgängig gemacht, was der „Last-in-First-out"-Intuition des Ressourcenlebenszyklus entspricht.
• Vergleich mit React useEffect Cleanup, RAII und Transaktions-Rollback: [Originale Schlussfolgerung des Papiers §7.3] React useEffect paart Effect strukturell mit Cleanup, aber Hooks dürfen nicht in Conditions/Loops/verschachtelten Funktionen aufgerufen werden, der Effect-Körper akzeptiert keine Async-Funktionen oder Iteratoren, und ein zusammengesetzter Inverse lässt sich aus bestehenden Effects nicht komponieren; RAII / lineare Typen beschränken Reversal auf einen lexikalischen Bereich; STM beschränkt Rollback auf das Transaktionsinnere; Cordis' Effects sind gewöhnliche Operationen, frei komponierbar, können asynchron sein, und verlangen nur, für jeden atomaren Effect einen Inverse zu schreiben — der zusammengesetzte Inverse wird durch Komposition automatisch abgeleitet.

ctx.effect verifiziert nicht die Korrektheit des Inverse

[Originale Schlussfolgerung des Papiers §3.1.3] ctx.effect verfolgt lediglich Inverses; es beweist nicht automatisch, dass ein Inverse korrekt ist. Die Witness-Bedingung g(δ) = γ ist eine Entwicklerpflicht, keine Laufzeitverifikation. Wenn ein Inverse falsch geschrieben ist (z. B. die falsche Ressource freigibt oder seine Seiteneffekte asymmetrisch zum Effect sind), schlägt Recovery fehl oder verschmutzt den Zustand, und die Laufzeit ist nicht verantwortlich.

Independence (Def 19) verlangt, dass die Transformationsmonoids zweier Effects miteinander kommutieren und den Inverse des jeweils anderen nicht stören — das ist die Voraussetzung, um das LIFO eines einzelnen Components auf verschachtelte Multi-Komponenten-Sequenzen zu verallgemeinern (Cor 21). Nicht-kommutative Effects (z. B. eine geordnete Operationskette) benötigen Coeffect-basierte Sortierung, um Recoverability zu garantieren.

Kern dieser Sektion

Theoretisches Konzept	Cordis-Implementierung
Unified Context Γ∞	ctx, First-Class-Kontext
Revertible Effect	ctx.effect(callback)
Inverse Accumulator	fiber.dispose
Witness-Bedingung g(δ)=γ	Entwicklerpflicht, von der Laufzeit nicht verifiziert
LIFO-Komposition ⋄	track ist ein Monoid-Homomorphismus (Thm 5)

Revertible Effects lösen „Rückgängigmachen" — aber Komponenten müssen auch „auf Abhängigkeitsänderungen reagieren". Letzteres lösen die Reactive Coeffects.