Component lifecycle and unload order

论文版本948a07b (main)

Revertible Effects solve "reverting"; Reactive Coeffects solve "perceiving dependency changes". For the two to coordinate on a component instance, a complete lifecycle state machine is needed. The paper §4.3 gives this mechanism, and Provider/Consumer unload order is the most important engineering detail.

Complete state machine

[Paper's original conclusion §4.3 Def 49] The complete lifecycle state machine of a component (fiber):

The seven L- primitives:

Primitive	Trigger	Semantics
L-Begin	target ≠ ⊥ and fiber in Inactive	Enter Reloading, record the committed view, start the effect iterator
L-Iter	In Reloading, target = ω, iterator yields Just(i')	Apply one iteration's effect, compose inverse into the accumulator
L-Finish	In Reloading, iterator yields Nothing	All effects installed, enter Active
L-Divert	In Reloading, target ≠ ω (dependency changed)	Abort/land the current iteration, enter Unloading (either abort, or land then unload)
L-Raise	Iteration throws error ξ	Enter Unloading carrying ξ; subsequent L-Unload applies the existing accumulator
L-Leave	In Active, target ≠ ω	Mark Unloading but do not apply inverse; stop providing coeffect
L-Unload	In Unloading, ¬ relied_n(γ)	Apply accumulator g, enter Inactive

Provider and Consumer unload order

[Paper's original conclusion §4.3.1] This is one of the most important engineering mechanisms in the paper. The base calculus's L-Unload puts "remove provision" and "run inverse" together, leaving no interval for the consumer's teardown. If the provider directly applies inverse to release resources while a consumer is still using the provider's dependency, you get crashes like "the database connection pool is closed while a transaction has not yet committed".

The paper introduces an Unloading intermediate state and a guard ¬ relied_n(γ) (no fiber still depends on n) to guarantee correct order:

1. L-Leave: Provider n marks Unloading, stops providing coeffect (its σ leaves the union of σ_γ), but keeps its own committed view and inverse untouched;
2. Consumer m detects that its dependency is about to disappear (target view becomes ⊥ or points to another fiber);
3. Consumer m uses the old dependency from its committed view to finish cleanup — because σ_γ only unions Active fibers, the binding of an Unloading fiber is invisible to other fibers, but the consumer's own committed view still points to it;
4. L-Unload runs when the guard ¬ relied_n(γ) is satisfied — i.e. all consumers depending on n have deactivated;
5. Provider n then runs its own inverse and releases resources.

This mechanism resolves:

• Waiting for connections to be returned before closing the pool
• Waiting for transactions to commit before closing the database
• Waiting for Agents currently using a Tool Provider before unloading it
• Cascading cleanup of child components when a parent exits

[Paper's original conclusion §4.4.4 Thm 66] The guard cannot deadlock: σ_γ only unions Active fibers; once L-Leave marks n, its table leaves σ_γ, no target view can point to n anymore, and all consumers committed to n are forced into their own teardown; the dependency graph propagates downward along the ≺ relation, and acyclicity + finiteness guarantees guard release (see the Progress theorem).

Inertia: what happens when dependencies change during async loading

[Paper's original conclusion §4.3.3] Modern effects are often asynchronous (fetch, file IO, sub-Agent calls). Once an iteration is in flight (an async Future), it must land, it cannot be aborted. When the target view changes during flight, L-Divert can only choose the "land then unload" branch; it cannot "abort the iteration" — once an iteration has been committed to a Future, it cannot be cancelled.

Three related concepts:

• Inertia: the in-flight transition handle, cannot be cancelled, can only wait to land;
• Iteration boundary: the granularity at which L-Divert intervenes — target change is only checked at iteration boundaries;
• Partial rollback: the accumulated inverse is applied, the unfinished part is rolled back;
• reload and unload interlink: after reload completes, if the target has changed, it chains into unload; after unload completes, if the target has changed, it chains into reload (Algorithm 5).

This mechanism guarantees that asynchronously loaded components will never end up "half old, half new" — either they finish entering Active, or they enter Unloading via L-Divert/L-Raise and roll back completely (corresponding to the Resolution Coherence theorem).

Theory-to-implementation correspondence

[Paper's original conclusion §5.1 Table 2] Mapping from the paper's formal concepts to the Cordis implementation:

Theoretical concept	Cordis implementation
Unified Context Γ∞	ctx, first-class context
Revertible Effect	ctx.effect(callback)
Coeffect register and access	ctx.set(key, value) / ctx.get(key)
Component Instantiation	ctx.use(component, config)
Dependency Specification	fiber.inject (i.e. the theoretical d)
Inverse Accumulator	fiber.dispose
Committed View	fiber.committed
Target View	fiber.target (recomputed by refresh)
Isolation	ctx.isolate(key, realm)
Interception	ctx.intercept(key, metadata)
Inertia	fiber.inertia (in-flight transition handle)
Lifecycle State	fiber.state (LOADING=Reloading, FAILED=Inactive(ξ))

Fiber vs React Fiber

[Inference based on the paper] The paper's Def 44 defines a fiber as one instantiation of a component, carrying (d, p, e, π, σ, τ, θ) — parent fiber, its own coeffect table, retirement marker, lifecycle state. It and React Fiber share only a name, not the concept: React Fiber is React's internal reconciliation unit, carrying component tree traversal state; Cordis Fiber is a component instance in the dynamic composition calculus, carrying the effect accumulator, committed view, and lifecycle state machine. Both borrow the "lightweight execution thread" sense of the word "fiber", but the theoretical frameworks are entirely different.

Next, look at what this mechanism guarantees at the metatheoretical level: Engineering translation of the formal theorems.