ADR-0015: Linear Lexical Algebraic Handlers for Core P1V3

Status: accepted
Date: 2026-07-25

Context

Core-N0 has typed effect rows but no canonical user-defined operation or handler semantics. The Surface bridge effect analyzer uses strings, Any, and host collections; it cannot define Core identity, typing, resumption, propagation, lifetime, or specialization behavior.

A general algebraic handler with first-class delimited continuations would immediately require continuation ownership, escape, cloning, multi-shot store semantics, and interaction with closure lifetimes. Those policies are not yet available. An abort-only handler would be simpler but would not establish effect-result substitution or a useful known-handler erasure path.

Options considered

Decision

Core profile P1V3 is a strict admission superset of P1V2. Existing profiles, semantic bytes, hashes, and rejection behavior remain unchanged.

P1V3 adds an inline canonical operation signature:

Operation<id, (ParameterTypes...), ResultType>

Operation identity is the numeric OperationId. Every occurrence of one ID in an artifact must carry exactly the same signature. Parameters and results cannot contain references or closures.

An unhandled operation is an explicit effect-row member:

Operation(signature)

and is performed by:

Perform(signature, arguments...)

A lexical handler contains:

• an explicit ordered capture vector;
• exact typed local bindings for those captures;
• one or more clauses in strictly increasing OperationId order;
• a handled body.

Each clause binds exactly the operation parameters and returns exactly the operation result type. Captures are the only outer values visible to clauses. There is no implicit host environment lookup.

Resumption semantics

The continuation from a Perform binder to the boundary of its selected Handle is structural and lexical. It is not a Core value.

• If the selected clause returns a value, that value replaces the Perform result and the captured continuation resumes exactly once.
• If the clause produces a typed error or an unhandled operation, the continuation resumes zero times and that outcome propagates.
• No syntax can resume twice, clone, store, compare, return, or pass the continuation.

This is an affine, implicit resumption policy. It deliberately establishes a sound lower bound before first-class continuations.

Handlers are deep for their handled body: after a successful clause return, the resumed continuation sees the same handler stack. A clause itself executes outside its own handler and all handlers nested inside that boundary. Therefore performing the same operation in a clause forwards to the next outer matching handler or becomes unhandled.

Effect subtraction and propagation

A matching active handler subtracts its operation from:

• a direct Perform;
• the declared effects of a direct call;
• the behavioral effects of a closure call.

All non-matching effects remain required in the enclosing function effect row. An operation that reaches the entry boundary is a canonical UnhandledOperation outcome containing its signature and evaluated arguments.

Operation arguments evaluate left-to-right. Handler captures evaluate left-to-right once when the lexical handler is entered. The innermost exact signature wins.

Lifetime and store interaction

Handler captures are explicit and local to the Handle term. Captured references must name active regions. They cannot escape because neither a handler nor its structural continuation is a value.

Calls executed while a handler environment contains a reference borrow the creator’s logical store. This keeps mutations through captured aliases visible and prevents a host-global store. A handler clause cannot reopen an already active captured region.

Identity and observability

Observable:

• operation ID, signature, argument values, and evaluation order;
• innermost-handler selection and forwarding;
• clause result, typed error, or unhandled operation;
• alias-visible mutation through explicit captures;
• deterministic call-depth and step-budget failure.

Not observable:

• host stack frames or continuation addresses;
• handler object identity;
• capture addresses or physical layout;
• continuation allocation, copying, or RC traffic.

Rationale

• Inline signatures preserve append-only encoding without adding a profile-wide declaration field that would change old hashes.
• Artifact-wide ID/signature consistency prevents dynamic casts and ambiguous operation identity.
• Explicit captures make handler environments deterministic and independently verifiable.
• Structural affine resumption provides useful effect elimination without inventing premature continuation ownership.
• Dynamic propagation across calls is necessary for lexical handlers to be semantically real rather than a local rewrite.

Trade-offs

• Clauses cannot abort with an ordinary replacement result for the whole handled computation; only typed error or unhandled propagation skips resumption.
• Continuations cannot be exposed, stored, cloned, or resumed manually.
• Multi-shot nondeterminism, generators, async suspension, and general control operators remain unavailable.
• Operation signatures are repeated inline, increasing artifact size.
• There is no return clause and no matching Surface syntax.

Consequences

Positive: Core-N0 gains typed operation identity, lexical handling, effect subtraction, dynamic call propagation, deterministic forwarding, and a specialization-friendly known-handler form without bridge dependencies.

Negative: P1V3 is not a complete algebraic-effects system.

Mitigation: unsupported continuation behavior has no representation; malformed signatures, capture mismatch, missing effects, duplicate clauses, inactive regions, and older-profile use fail closed.

Revisit trigger

Introduce an explicit continuation type only after affine ownership, escape, store snapshot/merge behavior, and region transfer are accepted. Add multi-shot continuation semantics only with a checked cloning policy. Add Surface handlers only after elaboration can produce exact operation signatures, ordered captures, and independently verified Core.