Linearity, typestate, and execution responsibility

Status: Not implemented; integration assessment for issue #149. Planning remains in B72. This page connects linear obligations, resolution scopes, and the existing typestate exploration; it does not approve an effects or concurrency redesign. Examples below are speculative pseudocode.

Recommendation and boundaries

Use small proposals with explicit interfaces: a linear ownership core (including its inseparable aggregate/error rules), a separate synchronous resolution-scope extension, and this integration contract. Keep the existing typestate exploration independent. No new effect syntax is required for concrete synchronous consumers. Propose effect-polymorphic resolution or suspension only when a concrete use cannot fit current certification or execution ownership.

The pages form independent review units where possible, not claims of complete implementation independence. Aggregate cleanup and failure ownership cannot be deferred from the linear core: a single discarded wrapper defeats the guarantee. Scope resolution depends on core preservation and terminal authority. Worker support depends on auditing runtime discard paths. Async completion depends on a responsible execution owner and suspension rules; it is not a core prerequisite.

Responsibility and dependency matrix

Counterexamples that test the split

A synchronous transaction with commit(tx) and rollback(tx) can carry a linear obligation using one nominal type and consuming free functions. It needs neither state-specialized methods nor effect annotations. Conversely, prepare(Draft) -> Ready is useful affine typestate even if discarding a draft or prepared value is harmless. Linearizing every state would add obligations without a corresponding product requirement.

Effects determine where an operation may execute, not whether it eventually executes. A worker-certified rollback may block forever; a locally permitted main-thread-only resolver can be meaningful even though worker certification rejects it. A function marked consuming is still not a terminal operation unless its ownership contract accounts for the seal and all failure paths.

Linear typestate with explicit errors

Consider a protocol whose contract requires a response or completed local cancellation after acceptance:

send(Request) -> Result[InFlight, SendError]
SendError = NotAccepted(Request, Cause) | Uncertain(InFlight, Cause)
receive(InFlight) -> Result[Response, ReceiveError]
ReceiveError = Retry(InFlight, Cause) | Finished(TerminalFailure)
request_cancel(InFlight) -> Result[Cancelling, CancelStartError]
CancelStartError = Retry(InFlight, Cause) | Finished(TerminalFailure)
finish_cancel(Cancelling) -> Result[Cancelled, CancelFinishError]
CancelFinishError = Retry(Cancelling, Cause) | Finished(TerminalFailure)

Here Request is affine before acceptance; InFlight and Cancelling are linear and carry the same obligation through transitions. Response, Cancelled, and TerminalFailure are ordinary values because this example’s contract considers their outcomes terminal. Another protocol may require a linear response body or recovery token instead. Uncertain acceptance cannot be reported as definitely unstarted when work may already exist remotely.

Typestate rejects calling finish_cancel on InFlight or receiving after the handle becomes Cancelling. Linearity rejects simply returning after a cancel request or discarding Retry(Cancelling, cause). Either mechanism alone misses the other’s error: an affine state may be abandoned; one linear runtime-state handle may still reject operation order only at runtime. Together they prevent abandonment and statically restrict these transitions, without proving that finish_cancel ever returns or that a remote peer received the cancellation.

Constructors must not let clients forge accepted or cancelled states. Moves prevent reuse of old handles, and terminal authority defines allowed outcomes. Use consuming free functions in experiments; current ordinary methods borrow receivers. For queues and runtime routing, an enum owning either linear state may be simpler than carrying state parameters through every helper. Input-driven parsers generally still suit runtime enums. See the existing typestate page for HTTP response lifecycles, field-extraction friction, and SQLite retry behavior.

Worker effects and hidden cleanup

Suppose an explicitly chosen resolver restores a process working directory:

restore(scope: DirectoryObligation) -> ():
    while True:
        match std.env.set_current_dir(scope.saved_path):
            Ok(()):
                authorized_restored(scope)
                return
            Err(cause):
                record_error(cause)           # retain scope and retry

worker(owner: DirectoryObligation):
    with resolving(owner, restore):
        compute()

This worker must be rejected: its required exit reaches a process-global effect. The example deliberately retries restoration failures and may never return; it does not silently treat failed restoration as success. The current effect checker already follows ordinary calls and destructors; generated consuming resolver calls must be visible in that same graph. A diagnostic should identify the submission/spawn, captured obligation, resolution scope, and call chain to set_current_dir, with the existing reason that it affects every thread. Report an ownership error as well if a proposed alternative merely drops the owner to avoid the forbidden call.

Do not classify all linear owners as main-thread-only. In principle a worker can compute while borrowing the data and leave resolution with a parent, or return the obligation through an ownership-preserving join protocol. Reject at worker certification when the reachable body/required cleanup needs the effect, and at transfer when the chosen worker API cannot preserve ownership on all paths. For the initial core, existing APIs that can discard such owners are ineligible regardless of whether the particular body appears safe.

Concrete resolvers with known bodies need no new effect annotations. A generic resolver specialized to a concrete callable can use existing certification only where the resulting calls are inspectable. Current indirect and boxed callable restrictions still apply; an erased resolver or unresolved higher-order call cannot claim worker safety just because its type says it consumes an owner. Such use needs either a statically inspectable adapter or a separately justified effect-contract extension. The limitation must appear at the requiring worker use and the hidden resolver call, not as an exemption for library cleanup.

Native workers and future completion

Current Future is affine. Dropping it neither cancels the job nor waits: accepted running work retains a worker owner and proceeds. Executor shutdown joins running workers, and ordinary shutdown drains accepted queued jobs. Cancellation of running work is cooperative; setting a token does not force termination or change a future’s result by itself.

These facts are useful execution machinery but do not make every stored value linear-safe. Preserve today’s APIs for discardable data. The first linear core should reject linear captures/results in existing thread, executor, channel, and lazy-frame paths that can destroy them, until a path-complete contract is implemented. This is a proposed restriction for new types, not a claim that today’s compiler knows Discardable.

A possible Completion[T] would specify those responsibilities explicitly; it must not silently redefine Future[T]. A joinable synchronous implementation could precede async/await. Submission failures preserve the job; cancellation must return it or complete its resolution; terminal results transfer to the consumer or an authorized resolver. All hidden resolvers require effect checks on the thread where they actually run, and must run without scheduler locks.

In future async work, moving a completion into .await merely transfers the obligation to the suspended frame. Dropping that frame cannot abandon it. A responsible scope/runtime must continue driving the computation or its cancellation to an allowed terminal outcome. async with or an async destructor provides a place to write suspending cleanup; neither ensures someone keeps executing it. The separate async/await exploration now examines suspension and execution ownership, but its affine spike does not support linear values or establish non-abandonment. Such syntax still needs a complete obligation-preserving runtime contract before claiming that guarantee.

A timeout can return immediately only by retaining responsibility elsewhere or returning the live owner. The responsible scope must retain all required owned resources and outlive any retained loans; a background cleanup cannot use a borrow into a caller that already returned. Completion can still wait forever, deadlock, or fail remotely. No fairness, termination, crash recovery, or bounded cancellation guarantee follows from linear ownership.

Integration checks before adoption

Demonstrate a synchronous linear transaction without new typestate/effect syntax, and an independently useful affine typestate API. Test the protocol above for illegal order, dropped retry states, and legal ownership-preserving retries. Worker compile-fail cases must include direct consumers, helper chains, inserted exit calls, and uncertified indirect resolvers. Positive worker tests must use permitted effects and an audited transfer protocol.

For every new worker protocol, inject start/submission failure, cancel queued work, drop the result consumer, exercise shutdown with pending/running work, and verify captures/results are resolved or returned exactly once. Include timeouts that return a live owner and reject a scope escaping required loans. Do not use a successful join or a cancellation flag as evidence of protocol completion. These checks bound any later implementation; this proposal adds no runtime or language behavior.