Capture Types and Capture-Set Polymorphism

Prerequisites. Direct starred prerequisites: Chapter 19, Chapter 50. No later core chapter depends on this route.

A closure can perform no effect when it is created and can outlive every region used during its creation, yet still retain authority. For example, let $c$ denote a printing capability and consider $$\lambda z.cz.$$ The latent print effect describes what a later call may do. A region annotation bounds where the closure may live. Neither annotation identifies the binding $c$ stored in the closure. The type of the value must record that binding. Capability calculi and affine borrowing systems make authority and aliasing explicit, but their judgments do not by themselves compute this closure capture [WCM00, RST20].

A capture-annotated core

The core calculus is , the capture-set extension of System  formalized by Boruch-Gruszecki, Brachthäuser, Lee, Lhoták, and Odersky [BGBL^+21]. A capture set is either a finite set $C=\{x_1,\dots ,x_n\}$ of term variables or the universal capture set $\star$. The finite empty set is $\varnothing$. Types and pretypes are distinct: The type $C▹U$ classifies a $U$-value whose free tracked variables are bounded indirectly by $C$. In particular, $\varnothing ▹U$ is pure. A type variable stands for a whole type and therefore is not a pretype.

The dependent arrow $\mathrm{\Pi }(x:S).T$ binds $x$ only inside capture sets in $T$. This restricted dependency is needed by the first useful polymorphic example. Let $$\mathsf{forward}=\lambda (f:\star ▹\mathrm{\Pi }(z:\varnothing ▹\mathrm{\top }).\star ▹\mathrm{\top }).f.$$ Its precise result type is $$\varnothing ▹\mathrm{\Pi }(f:\star ▹\mathrm{\Pi }(z:\varnothing ▹\mathrm{\top }).\star ▹\mathrm{\top }).\{f\}▹\mathrm{\Pi }(z:\varnothing ▹\mathrm{\top }).\star ▹\mathrm{\top }.$$ The singleton $\{f\}$ says that the returned value captures no more than the argument supplied for $f$; it does not assert that the result captures every variable captured by every possible argument.

Capture-set substitution replaces a variable by a set: It extends homomorphically through types and through type annotations in terms. Ordinary term substitution remains postfix and capture avoiding.

Indirect bounds and subcapturing

Subset inclusion is insufficient because a variable can stand for a value with a smaller capture. The judgment $\mathrm{\Gamma }⊢C_1{\preccurlyeq }_{\mathsf{cap}}{C}_2$ is the least relation generated by

$\mathrm{\Gamma }⊢C{\preccurlyeq }_{\mathsf{cap}}\star$

$\mathrm{\Gamma }⊢\{x_i\}{\preccurlyeq }_{\mathsf{cap}}C(1\le i\le n)$

$\mathrm{\Gamma }⊢\{x_1,\dots ,x_n\}{\preccurlyeq }_{\mathsf{cap}}C$

$1\le i\le n$

$\mathrm{\Gamma }⊢\{x_i\}{\preccurlyeq }_{\mathsf{cap}}\{x_1,\dots ,x_n\}$

$x:T\in \mathrm{\Gamma }$$\mathrm{\Gamma }⊢\mathrm{cv}(T,\mathrm{\Gamma }){\preccurlyeq }_{\mathsf{cap}}C$

$\mathrm{\Gamma }⊢\{x\}{\preccurlyeq }_{\mathsf{cap}}C$

Reflexivity and transitivity are admissible; they are not primitive rules.

Proof of Lemma 51.2 — Subcapturing preorder

Proof. For reflexivity, split a finite capture set by SC-Set-L and reinsert each singleton by SC-Set-R; the universal case is SC-Star.

For transitivity, induct on the first derivation. A last SC-Star can be followed only by a judgment whose right side is universal, so SC-Star closes the composite. A last SC-Set-L composes each singleton premise and rebuilds the finite left side. For a last SC-Set-R, invert the second derivation: SC-Star closes immediately, SC-Set-L exposes the selected singleton premise, and when the intermediate set is itself a singleton the second derivation already has the required source. A last SC-Var first composes its declared capture bound with the second derivation, then reapplies SC-Var. Each recursive call removes the last rule of the first derivation, so the induction terminates. ◻

Let $\mathrm{\Gamma }=y:\varnothing ▹\mathrm{\top },x:\star ▹\mathrm{\top }$. Then $$\mathrm{\Gamma }⊢\{x,y\}{\preccurlyeq }_{\mathsf{cap}}\{x\}.$$ The $x$-premise follows from SC-Set-R. For $y$, rule SC-Var reduces the goal to $\varnothing {\preccurlyeq }_{\mathsf{cap}}\{x\}$, which SC-Set-L derives with no singleton premises. Thus a pure binding can be removed from a capture bound.

The converse indirect step need not hold. If $x:\{y\}▹U\in \mathrm{\Gamma }$, then $\mathrm{\Gamma }⊢\{x\}{\preccurlyeq }_{\mathsf{cap}}\{y\}$ follows by SC-Var; no rule derives $\{y\}{\preccurlyeq }_{\mathsf{cap}}\{x\}$ unless the context gives an independent path from $y$ to $x$.

Proof of Lemma 51.3 — Finite subcapturing decomposition

Proof. The reverse implication is SC-Set-L. For the forward implication, compose the premise with $\mathrm{\Gamma }⊢\{x_i\}{\preccurlyeq }_{\mathsf{cap}}C$, derived by SC-Set-R, and use admissible transitivity. ◻

Typing and the capture-polymorphic application

Type subtyping separates outer capture bounds from pretype structure. Its decisive rules are The function rule is contravariant in its domain and covariant in its codomain: The ordinary rules govern $\mathrm{\top }$, bounded universal types, variables, reflexivity, and transitivity.

The term rules that expose capture information are

$x:C▹U\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x:\{x\}▹U$

$x:X\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x:X$

$\mathrm{\Gamma },x:S⊢t:T$$\mathrm{\Gamma }⊢\mathrm{\Pi }(x:S).T\mathsf{wf}$

$\mathrm{\Gamma }⊢\lambda (x:S).t:\mathrm{fv}(\lambda (x:S).t)▹\mathrm{\Pi }(x:S).T$

$\mathrm{\Gamma }⊢t:C▹\mathrm{\Pi }(x:S).T$$\mathrm{\Gamma }⊢s:S$

$\mathrm{\Gamma }⊢ts:T[\mathrm{cv}(S,\mathrm{\Gamma })/x]$

$\mathrm{\Gamma }⊢S\mathsf{wf}$

$\mathrm{\Gamma }⊢t[S]:T[S/X]$

$\mathrm{\Gamma }⊢t:T$

$\mathrm{\Gamma }⊢t:S$

Rule Var-C records the binding $x$, not the bound $C$ attached to its declared type. Rule App-C later replaces $x$ in the codomain by the argument type’s capture bound. This pair of choices is the mechanism of capture-set polymorphism.

Let $g:\{c\}▹\mathrm{\Pi }(z:\varnothing ▹\mathrm{\top }).\star ▹\mathrm{\top }$. Applying $\mathsf{forward}$ to $g$ yields The equality unfolds definition 51.1 and capture-set substitution. The function’s own empty capture is discarded by App-C; the returned value retains exactly the upper bound of its argument.

These rules also delimit inference. With all parameter, bound, and pretype annotations supplied, Var-C generates a singleton, Abs-C computes free variables, and App-C substitutes the argument bound. Subsumption may then widen the result. Thus local capture bounds are calculable, but the declarative calculus states no principal-type or annotation-inference theorem. Rule Var-X is a deliberate precision boundary: because $X$ is a type and not a pretype, the grammar has no type $\{x\}▹X$.

Reduction, variance, and substitution

Call-by-value beta reduction substitutes both the value and its exact free variables: $$(\lambda (x:S).t)v{⟶}_{\mathsf{cap}}t[\mathrm{fv}(v)/x][v/x].$$ The capture-set substitution acts only in annotations; the term substitution acts only in term positions. Type beta and evaluation-context congruence are as in call-by-value .

Typing an application uses the possibly widened set $\mathrm{cv}(S,\mathrm{\Gamma })$, whereas reduction uses the exact set $\mathrm{fv}(v)$. The relation between them is subcapturing, not equality. Consequently, a variable bound by $\mathrm{\Pi }(x:S).T$ may occur in capture annotations of $T$ only covariantly with respect to that binder. The well-formedness judgment $\mathrm{\Gamma };A_{+};A_{-}⊢T\mathsf{wf}$ records the variables permitted in positive and negative positions; an arrow swaps $A_{+}$ and $A_{-}$ in its domain and adds its binder to $A_{+}$ in its codomain.

The restriction is load bearing. Consider $$f=\lambda (x:\star ▹U).\lambda (y:\{x\}▹U).y.$$ If the negative occurrence of $x$ in the inner parameter type were allowed, a pure $v:\varnothing ▹U$ could first be widened to $\star ▹U$. Static application would then assign a domain $\star ▹U$ to the reduct. Beta reduction instead substitutes $\mathrm{fv}(v)=\varnothing$, producing a function whose domain is $\varnothing ▹U$. Function subtyping reverses domains, so the latter type is not a subtype of the former.

Proof of Lemma 51.4 — Covariant capture substitution

Proof. Use simultaneous induction on the formation of types and pretypes. For an outer capture annotation containing $x$, capture-set substitution replaces $x$ by $C_1$ and $C_2$; Capt applies to the assumed subcapturing derivation. In an arrow domain the polarity sets exchange, so $x$ is not available in the positive set and cannot occur there. In the codomain the binder formation rule places $x$ only in the positive set, where the induction hypothesis gives covariance. Bounded universal types repeat the arrow argument with a type-variable binder. The $\mathrm{\top }$ and type-variable cases contain no capture occurrence. ◻

Proof of Lemma 51.5 — Capture bound of a value

Proof. Induct on the value-typing derivation. If its last introduction is Abs-C or TAbs-C, the outer annotation is exactly $\mathrm{fv}(v)$, and reflexivity applies. If the last rule is Sub-C, the induction hypothesis bounds the free variables by the smaller type’s outer capture. Inversion of outer type subtyping gives the subcapturing premise to the larger annotation; admissible transitivity composes the two bounds. These are the only last rules for a value. ◻

Proof of Lemma 51.6 — Value substitution

Proof. Induct on the typing derivation of $t$. The variable case $t=x$ uses the precise-capture typing of values: some pretype $U$ satisfies . The abstraction case chooses its bound variable outside $\mathrm{fv}(v)\cup \mathrm{dom}(\mathrm{\Gamma })\cup \{x\}$, applies the induction hypothesis to the opened body, and reconstructs Abs-C. In the application case, capture-set substitution composes with the codomain substitution from App-C. The induction hypotheses reconstruct both premises. Finally, lemma 51.5 gives $\mathrm{\Gamma }⊢\mathrm{fv}(v){\preccurlyeq }_{\mathsf{cap}}\mathrm{cv}(S,\mathrm{\Gamma })$; lemma 51.4 and Sub-C widen the exact reduct type to the stated static type. Type abstraction, type application, and subsumption repeat these three mechanisms with the corresponding System  substitution or transitivity lemma. ◻

Proof of Theorem 51.7 — Preservation and progress for

Proof. For preservation, induct on the reduction rule. Congruence cases rebuild the typing rule after applying the induction hypothesis. Type beta uses ordinary type substitution. Term beta uses lemma 51.6; its conclusion is exactly the result type printed by App-C.

For progress, induct on the closed typing derivation. Subsumption invokes the induction hypothesis. In an application, either the function steps, the argument steps after the function is a value, or both are values. By canonical forms for the capture-annotated arrow, the function is a term abstraction, so term beta applies. Type application uses the corresponding canonical form for a bounded type abstraction. Variables cannot occur in an empty context. ◻

The source’s Coq development proves the full versions of these lemmas, including weakening, narrowing, type substitution, and the polarity-indexed formation infrastructure. The local proof isolates the nonstandard term-beta case; the complete mechanized development owns the remaining cases.

Proof of Theorem 51.8 — Capture prediction

Proof. Repeated preservation gives $\mathrm{\Gamma }⊢v:T$. Apply lemma 51.5. ◻

Capture prediction is an upper-bound theorem. It does not state literal set inclusion, because SC-Var follows indirect capture bounds.

Hiding, tunneling, and escape

Bounded type variables provide the core’s one hiding mechanism. In rule Var-X retains the abstract type $X$, rather than manufacturing an ill-formed annotation $\{x\}▹X$. Instantiating $X$ later restores the complete argument type. Capture information can therefore tunnel through this parametric term while it is hidden by $X$. The price is exact: the core cannot express capture-polymorphic data structures whose element is an abstract type variable with a fresh outer capture annotation. This is not the boxed tunneling discipline of later capture calculi, and no theorem about those calculi is imported into .

A separate boxed capture card

Fourment and Xu’s changes both the type grammar and the operational signature [FX23]. Its pure types include type variables, $\mathrm{\top }$, arrows, bounded universals, and boxed captured types $◻(C▹R)$; a captured type has the outer form $C▹R$. Type application accepts a pure type. A captured argument must therefore be boxed first and recovered explicitly by an unbox term whose written capture set is in scope. This is the boxed tunneling discipline. It is not the abstract-type tunneling derived above.

The boxed calculus is in monadic normal form. Its machine states are $\mathrm{\Sigma }=⟨S\mid E\mid e⟩$, with a value store $S$, a list of continuations $E$, and a focused expression $e$. Write $\mathrm{\Sigma }{\mathsf{ok}}_{◻}V$ for the source artifact’s state-typing judgment: some environment types the store, the continuation from the focused type to $V$, and the focused expression at that focused type. A final state has the form $⟨S\mid \varnothing \mid a⟩$ for an answer $a$.

Proof of Theorem 51.9 — Mechanized boxed-state safety

Mechanized import. The theorem is the direct reading of preservation and progress in the pinned Coq development. The paper’s Figures 2–5, on physical pages 4–6, fix the pure/captured grammar, well-formedness, and machine reductions. The artifact’s CCsub_Soundness.v lines 273–276 and 529–532 state the two results. No boxed rule or theorem is used in the preceding proofs. ◻

The paper’s non-local-return and region extensions turn capture prediction into an escape check. Their delimiter rule binds a local capability $k$ and requires the non-derivability condition $$\mathrm{\Gamma },k:\star ▹\mathsf{Return}[T]⊬\{k\}{\preccurlyeq }_{\mathsf{cap}}\mathrm{cv}(T,\mathrm{\Gamma }).$$ If a returned value contains $k$ free, capture prediction would derive the forbidden judgment. The condition therefore excludes that return. This extension is not a new theorem of the core: it adds capability syntax, dynamics, and typing rules before applying the core prediction theorem.

Capture sets are not effect rows, region sets, ownership quantities, or proofs that an authority is safe to exercise. They bound the tracked bindings retained by values. The selected source proves no closure-conversion theorem, so this chapter makes no claim that a particular environment layout preserves typing or reduction.

Sources.

The archived paper’s PDF pages 5–6 print syntax, reduction, and subcapturing; pages 9–11 print the polarity condition, progress, preservation, prediction, and the two capture-substitution lemmas; pages 14–15 print the non-local-return escape argument. Its archived Coq 8.10.0 sources contain the complete formal development: CFsub_Soundness.v lines 2033–2285 prove covariant capture substitution, lines 2924–2990 prove value substitution, and lines 3325 and 3424 begin preservation and progress [BGBL^+21]. The Scala reference supplies surface examples only and is not theorem evidence. The paper’s printed SC-Var premise uses $\mathrm{\Gamma }⊢x:T$; this chapter follows the pinned locally nameless mechanization’s environment-lookup premise, written $x:T\in \mathrm{\Gamma }$, and does not transfer the paper theorem across any other change of signature.