ADR-0014: Bounded Existential Closures for Core P1V2

Status: accepted
Date: 2026-07-25

Context

Core-N0 already represents the behavioral type Closure<(Args...), Effects, Result>, but P1V0 and P1V1 reject closure values. T2B deliberately accepts only closed direct functions. Stage 1 cannot claim closure semantics until capture order, hidden environment typing, call effects, recursion, aliasing, and environment lifetime are checked by the canonical verifier.

A host Rc<Environment>, pointer to a stack frame, dynamic dictionary, or Surface runtime closure would import bridge representation into canonical semantics. Conversely, admitting escaping reference captures before region arguments and ownership transfer exist would make the lifetime model unsound.

Options considered

Decision

Core profile P1V2 is a strict admission superset of P1V1. Existing P1V0/P1V1 bytes, hashes, and rejection behavior remain unchanged.

P1V2 adds two ANF rvalues:

PackClosure(function, captures...)
CallClosure(closure, arguments...)

For captures with ordered types (C0, C1, ... Cn), PackClosure is valid only when the selected code function has the exact signature:

FunctionId<(Tuple<C0, C1, ... Cn>, Args...), Effects, Result>

The produced value has behavioral type:

Closure<(Args...), Effects, Result>

The environment type is existential at the behavioral boundary:

exists Env.
    (FunctionId<(Env, Args...), Effects, Result>, Env)

P1V2 fixes Env to one ordered tuple in the canonical packed representation. Capture names are absent. Capture sequence order is semantic, deterministically encoded, and is the tuple-field order observed by closure code.

PackClosure is semantically pure. It constructs a value and does not imply a physical heap allocation, RC increment, stack placement, or Alloc<rho> effect. A later backend may erase, scalar-replace, stack-place, or otherwise represent the environment while preserving behavior.

CallClosure injects the packed environment as the code function’s first argument, evaluates explicit arguments left-to-right, and requires the caller effect row to contain every effect in the behavioral closure type.

Bounded type and lifetime rules

The first profile admits capture elements already admitted by P1V2, including Shared scalar references, tuples, sums, scalars, and read-only Array<F64>. A captured reference must name a currently active lexical region.

Closure values are local-only:

• a Closure may not occur recursively in a function parameter or result;
• a Ref may not occur recursively in the entry parameters or any function result;
• nested closure capture is rejected;
• reference-containing closure environments may enter closure code only through the hidden environment parameter;
• a closure cannot be placed in a P1V2 logical-store cell because cells remain scalar-only.

Consequently a captured reference cannot outlive the lexical Region that was active when the closure was packed. Closure calls with reference-containing environments borrow the creator’s logical store for the duration of the call. The code function sees captured reference regions as active borrowed regions; it cannot reopen the same region.

Ordinary direct calls with reference-containing arguments use the same borrowed-store rule. Reference-containing tail calls are rejected in this bounded profile so the evaluator never transfers a borrowed lifetime into a fresh tail-call frame.

Closure code may recurse with an explicit environment through ordinary direct calls. This admits recursive closure behavior without admitting a cyclic self-reference inside the environment. Recursion remains bounded by the canonical call-depth and step budgets.

Identity and observability

There is no closure equality, code-pointer observation, capture-address observation, environment-layout query, destructor, or finalizer.

Observable:

• capture order and captured values;
• behavior of mutation through a captured alias;
• argument/effect order;
• function result or typed error;
• declared evaluation-budget failure.

Not observable:

• host closure representation;
• environment allocation count or address;
• code address;
• RC traffic;
• environment placement or scalar replacement.

Rationale

• The selected code function proves the hidden environment type rather than trusting a dynamic cast.
• Ordered capture tuples produce stable hashes without Surface names.
• Local-only closure values establish a sound first lifetime boundary without choosing an escaping ownership model.
• Borrowing the active logical store preserves captured alias behavior without a hidden global heap.
• Explicit environment recursion exercises closure conversion while avoiding cyclic closure construction.

Trade-offs

• Closures cannot yet be returned, passed as arguments, nested, stored, or called in tail position.
• Value-only closures are also local-only even where escape could be safe.
• Reference-containing tail recursion remains unavailable.
• The first environment representation is a tuple rather than an arbitrary user-defined ADT.
• No matching Surface capture syntax is admitted yet.

Consequences

Positive: Core-N0 gains deterministic, typed, effect-aware closure behavior with alias-preserving captured references and no dependency on bridge closure representation.

Negative: the profile is deliberately insufficient for first-class escaping functional programs.

Mitigation: unsupported escape, nested closure, environment mismatch, inactive capture region, missing effect, and borrowed tail transfer fail closed.

Revisit trigger

Admit escaping closures only after closure lifetime/ownership transfer and region arguments are explicit. Admit tail closure calls only after borrowed region transfer is modeled. Admit cyclic recursive closures only after the accepted RC/cycle policy has a checked representation. Surface captures remain blocked until elaboration can derive the exact ordered environment and pass Core verification independently.