Chapter 31Core route

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Chapter 22 recorded effects in finite sets. A set says which operations may occur, and it is the right abstraction for the semantic arguments made there. But it forgets how many copies of a label a type contains. That loss is harmless until a handler, an operator that interprets selected requests, removes one occurrence of a label while permitting another occurrence to escape.

Effect rows retain those occurrences as finite multisets with a possibly open tail. Thus $⟨ raise, raise ∣ μ ⟩ ⧸ \equiv ⟨ raise ∣ μ ⟩ .$ Read $⟨ ℓ ∣ ε ⟩$ as the label $ℓ$ consed onto the row $ε$ ; the vertical bar separates the visible prefix from its tail. The duplicate is not decoration. A handler can consume the first occurrence and leave the second in its result effect. The same convention also gives a small, unconstrained unification algorithm: there is no separate “lacks” predicate saying that a tail does not contain a given label.

The transaction whose tail stays open

Fix the operation declarations used by the transaction. $\begin{array}{rcl} get & : & 1 ⇝ Int, \\ put & : & Int ⇝ 1, \\ raise & : & Error ⇝ 0, \\ \log & : & Error ⇝ 1 . \end{array}$ For a callback $f$ , use the core computation; the saved value $s$ witnesses the initial read, while the callback’s result is committed by $put$ : $\begin{array}{l} t_{f} = perform get () to s . \\ f () to x . \\ perform put x to u . \\ return x . \end{array}$ The callback has different principal signatures when it is let-polymorphic and when it is a first-class monomorphic argument. Put $\begin{matrix} (31.1) & \begin{aligned} E_{μ} & = ⟨ get, put, raise ∣ μ ⟩, \\ G_{μ} & = ⟨ get, put ∣ μ ⟩ . \end{aligned} \end{matrix}$ Write $τ! ε$ for the type of a computation that returns a value of type $τ$ and performs the effects listed in the row $ε$ ; in chapter 22 the same separator instead carried a finite set of operations. If $Γ_{f} = f : \forall ν . 1 \overset{⟨ raise ∣ ν ⟩}{\to} Int,$ then the occurrence of $f$ in $t_{f}$ instantiates $ν = ⟨ get, put ∣ μ ⟩$ , and $\begin{matrix} (31.2) & Γ_{f} ⊢ t_{f} : Int! E_{μ}, {gen}_{c} (Γ_{f}, Int! E_{μ}) = \forall μ . (Int! E_{μ}) . \end{matrix}$ Here ${gen}_{c} (Γ, τ! ε)$ quantifies every type and row variable free in $τ! ε$ but not in $Γ$ . If instead we form the value $λ f . t_{f}$ , its parameter is monomorphic, so its principal scheme is $\begin{matrix} (31.3) & \forall μ . (1 \overset{G_{μ}}{\to} Int) \overset{G_{μ}}{\to} Int . \end{matrix}$ The lambda-bound $f$ has no declared $raise$ effect; only the $get$ and $put$ actually performed by $t_{f}$ remain. The row $E_{μ}$ is a legal instance of this more general scheme, obtained by taking the tail of $G$ to begin with $raise$ , but it is not principal for the wrapper. Giving a first-class argument its own quantified row scheme would require higher-rank row polymorphism, which this Hindley–Milner core does not have. In both signatures $μ$ is open, so callers may add logging or allocation effects.

Now compare two exception handlers. A fallback handler applied at the principal instance $E_{μ}$ removes $raise$ and leaves $⟨ get, put ∣ μ ⟩$ . A rethrowing handler must instead leave one $raise$ in its output. It therefore asks for two occurrences in its input, one to consume and one to re-perform. The principal row of $t_{f}$ admits that instance by taking $μ = ⟨ raise ∣ ν ⟩$ . Its input row is then $⟨ get, put, raise, raise ∣ ν ⟩$ ; the rethrowing handler removes one occurrence and leaves $⟨ get, put, raise ∣ ν ⟩$ for an outer handler.

Rows are multisets, not sets

Definition 25.1 — Effect rows and equivalence ¶

Let labels $ℓ$ range over a fixed finite operation signature $Σ$ , with $Σ (ℓ) = P_{ℓ} ⇝ R_{ℓ}$ . Every declared $P_{ℓ}$ and $R_{ℓ}$ is a closed, well-kinded type; in particular, type or row substitution never changes an operation declaration. Type variables are written $α$ , and row variables $μ$ . Kinds keep the two sorts apart. $κ ::= * ∣ R, α :: *, μ :: R .$ The kind $*$ classifies ordinary value types and $R$ classifies effect rows. A substitution is kind preserving when it maps $*$ -variables to types and $R$ -variables to rows. $\begin{array}{rcl} τ & ::= & α ∣ b ∣ τ \overset{ε}{\to} τ, \\ ε & ::= & μ ∣ ⟨ ⟩ ∣ ⟨ ℓ ∣ ε ⟩, \\ σ & ::= & \forall \bar{α} \bar{μ} . τ, \\ χ & ::= & \forall \bar{α} \bar{μ} . (τ! ε) . \end{array}$ We abbreviate nested extensions by $⟨ ℓ_{1}, ℓ_{2} ∣ ε ⟩$ . A closed row has no row variable. It is duplicate-free when no label occurs twice. The base types $b$ include $0, 1, Bool, Int$ , $Error$ , and $Env$ . Contexts assign value schemes $σ$ to variables. A computation scheme $χ$ records both inferred outputs; it is used to state principality, not as a context entry. Constants range over a fixed signature $C$ . Every declaration $C (c) = \forall \bar{α} \bar{μ} . τ$ is closed and well kinded: all free variables of $τ$ are bound by the displayed quantifiers. Define $\begin{aligned} ftv (τ! ε) & = ftv (τ) \cup ftv (ε), \\ {gen}_{c} (Γ, τ! ε) & = \forall (ftv (τ! ε) ∖ ftv (Γ)) . (τ! ε), \\ {gen}_{v} (Γ, τ) & = \forall (ftv (τ) ∖ ftv (Γ)) . τ . \end{aligned}$

The row equivalence is the least congruence generated by adjacent exchange: $\begin{matrix} (31.4) & ⟨ ℓ_{1}, ℓ_{2} ∣ ε ⟩ \equiv ⟨ ℓ_{2}, ℓ_{1} ∣ ε ⟩ . \end{matrix}$ Here $\equiv$ is finite-multiset equivalence of effect rows and its congruential extension to the displayed types and contexts; it is not the book’s judgmental-equality relation. There is deliberately no contraction equation. Equality of closed rows is therefore equality of finite multisets. A substitution is kind preserving; its application is homomorphic and row equality is always read modulo $\equiv$ . No side condition $ℓ_{1} \neq ℓ_{2}$ is needed in the exchange equation: when the two labels agree, it is simply an identity. Extend $\equiv$ congruentially to types: base types and variables are equivalent only to themselves, and $A_{1} \overset{ε_{1}}{\to} B_{1} \equiv A_{2} \overset{ε_{2}}{\to} B_{2}$ exactly when $A_{1} \equiv A_{2}$ , $ε_{1} \equiv ε_{2}$ , and $B_{1} \equiv B_{2}$ . Context equivalence is pointwise on the bodies of schemes, after alpha-renaming bound variables. Thus $T Γ \equiv Q S Γ$ below is a pointwise statement, not literal syntax equality.

Referenced from 4 locations

For a row $ε$ , write $M (ε) : Σ \to N$ for the multiplicity function of its visible prefix. A variable or empty tail contributes zero, and $+$ denotes pointwise addition. This notation will support both cancellation and the unification guard.

Lemma 25.2 — Cancellation ¶

For a label $ℓ$ , $⟨ ℓ ∣ ε_{1} ⟩ \equiv ⟨ ℓ ∣ ε_{2} ⟩ ⟹ ε_{1} \equiv ε_{2} .$ More generally, if $ℓ \notin L$ and $⟨ L ∣ ε ⟩ \equiv ⟨ ℓ ∣ δ ⟩$ , then $ε \equiv ⟨ ℓ ∣ ε^{'} ⟩$ for some $ε^{'}$ .

Referenced from 6 locations

Proof of Lemma 25.2 — Cancellation

Proof. Every row has a normal form $⟨ L ∣ t ⟩$ , where $L$ is a finite multiset of visible labels and the tail atom $t$ is either one row variable or $⟨ ⟩$ . Bubble-sorting adjacent labels in a fixed total order proves $⟨ L ∣ t ⟩ \equiv ⟨ L^{'} ∣ t^{'} ⟩ ⟺ L = L^{'} as multisets and t = t^{'} .$ Exchange leaves the multiplicity function $M$ and the tail atom unchanged, so equivalent rows have equal multiplicities and equal tails; bubble sort gives the converse. The first claim subtracts one from the multiplicity of $ℓ$ on both sides. For the second, the right side has positive $ℓ$ -multiplicity and the prefix $L$ contributes none, so the tail contributes at least one. Exchange moves that occurrence to its head. ◻

Unique-label rows require an absence constraint such as $ℓ \notin μ$ when unifying $⟨ ℓ ∣ μ ⟩$ . Here duplicates are legal, so ordinary substitutions suffice.

The two row systems have the following exact division of labor.

	record rows of chapter 4	effect rows here
duplicates	forbidden	retained
tail obligation	$ℓ \notin μ$	common-tail guard in the unifier
equality	exchange plus uniqueness	multiset exchange
exposure	$insert$ with lacks	$rewrite$ without lacks
elimination	select one unique field	handle one occurrence

The two mechanisms prevent the same cyclic exposure in different places: Chapter 4 records a lacks predicate in the type, whereas this chapter checks a common-tail guard during unification. See also the scoped-duplicate comparison in subsection 7.8.2; effect multiplicity is a deliberate equational choice, not a novel exposure algorithm. Swapping the equalities is unsound: contraction would erase the distinction between a handled occurrence and a re-performed one, while allowing duplicate record labels would make field selection ambiguous.

Exercise 25.1 — No contraction ¶

★☆☆ Give a multiplicity model separating $⟨ ℓ, ℓ ∣ μ ⟩$ from $⟨ ℓ ∣ μ ⟩$ . Explain why a handler that re-performs $ℓ$ makes the distinction observable at the type level.

Referenced from 3 locations

A fine-grain call-by-value core

Definition 25.3 — Fine-grain effect-row calculus ¶

Values and computations are separate: $\begin{array}{rcl} v & ::= & x ∣ c ∣ λ x . e, \\ e & ::= & return v ∣ v v ∣ e to x . e ∣ perform ℓ v \\ ∣ handle e with H ∣ let x = e in e, \\ H & ::= & {return x \mapsto e_{r}; ℓ_{i} (p_{i}; k_{i}) \mapsto e_{i}}_{i = 1}^{n} . \end{array}$ This separation of syntactic value forms from computations, together with elimination forms that take values, is what fine-grain call by value means here. Unlike CBPV in chapter 22, this core has no $thunk$ / $force$ type boundary. The handled labels $ℓ_{1}, \dots, ℓ_{n}$ are distinct. The judgments are $Γ ⊢_{v} v : τ$ and $Γ ⊢ e : τ! ε$ . Instantiation at a variable is implicit. Constants $c$ are base constructors with fixed closed schemes; all function values in the core are lambdas. For $H = {return x \mapsto e_{r}; ℓ_{i} (p_{i}; k_{i}) \mapsto e_{i}}_{i = 1}^{n}$ , write $handled (H) = {ℓ_{1}, \dots, ℓ_{n}}$ .

x : \forall \bar{α} \bar{μ} . τ \in Γ

T instantiates only \bar{α}, \bar{μ}

Γ ⊢_{v} x : T τ

V-Var

C (c) = \forall \bar{α} \bar{μ} . τ

T instantiates only \bar{α}, \bar{μ}

Γ ⊢_{v} c : T τ

V-Const

Γ, x : τ_{1} ⊢ e : τ_{2}! ε

Γ ⊢_{v} λ x . e : τ_{1} \overset{ε}{\to} τ_{2}

V-Lam

Γ ⊢_{v} v : τ

Γ ⊢ return v : τ! ε

C-Return

Γ ⊢_{v} v_{1} : τ_{1} \overset{ε}{\to} τ_{2}

Γ ⊢_{v} v_{2} : τ_{1}

Γ ⊢ v_{1} v_{2} : τ_{2}! ε

C-App

Γ ⊢ e_{1} : τ_{1}! ε

Γ, x : τ_{1} ⊢ e_{2} : τ_{2}! ε

Γ ⊢ e_{1} to x . e_{2} : τ_{2}! ε

C-To

Σ (ℓ) = P_{ℓ} ⇝ R_{ℓ}

Γ ⊢_{v} v : P_{ℓ}

Γ ⊢ perform ℓ v : R_{ℓ}! ⟨ ℓ ∣ ε ⟩

C-Op

Only C-Return and C-Op may choose their row tails freely. There is no general effect-weakening rule; in particular, an application has exactly the latent row written on its function type. Because C-Return and C-Op may choose any tail, both arms of a sequence can be typed at one common effect. Let-generalization is restricted to pure computations:

Γ ⊢ e_{1} : τ_{1}! ⟨ ⟩

\bar{a} = ftv (τ_{1}! ⟨ ⟩) ∖ ftv (Γ)

Γ, x : \forall \bar{a} . τ_{1} ⊢ e_{2} : τ_{2}! ε

Γ ⊢ let x = e_{1} in e_{2} : τ_{2}! ε

C-Let

Here $\bar{a}$ contains variables of both kinds. Effectful sequencing uses $to$ , whose bound variable is monomorphic. This is also the surface elaboration policy. A source $let$ is accepted as the core $let$ form only when inference can unify the bound computation’s row with $⟨ ⟩$ ; an effectful source binding must instead elaborate to core $to$ , and is monomorphic. Thus the core syntax records, rather than retrospectively guesses, the generalization decision.

The sole conversion rule changes only the row annotation:

Γ ⊢ e : τ! ε

ε \equiv ε^{'}

Γ ⊢ e : τ! ε^{'}

C-RowConv

Hence all typing rules are stable under row equivalence. In particular, the effect in C-To need only be equivalent in its two premises; this is a consequence of C-RowConv, not a second conversion convention.

Referenced from 2 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Rule C-Let is already visible on a closed term. If $Γ ⊢_{v} 0 : Int$ , write $C_{0} = Int! ⟨ ⟩, e_{0} = let x = return 0 in return x .$ Then $\frac{\begin{matrix} \frac{Γ ⊢_{v} 0 : Int}{Γ ⊢ return 0 : C_{0}} C - Return \\ ftv (C_{0}) ∖ ftv (Γ) = \emptyset \\ \frac{Γ, x : Int ⊢_{v} x : Int}{Γ, x : Int ⊢ return x : C_{0}} C - Return \end{matrix}}{Γ ⊢ e_{0} : C_{0}} C - Let .$ The generalized-variable set is empty here; replacing (0) by a polymorphic pure value exercises the same rule with a nonempty set.

Definition 25.4 — Handler typing ¶

The handler rule removes exactly one occurrence of each handled label.

Γ ⊢ e : A! ⟨ ℓ_{1}, \dots, ℓ_{n} ∣ ε ⟩

Γ, x : A ⊢ e_{r} : B! ε

(Σ (ℓ_{i}) = P_{i} ⇝ R_{i})_{i = 1}^{n}

(Γ, p_{i} : P_{i}, k_{i} : R_{i} \overset{ε}{\to} B ⊢ e_{i} : B! ε)_{i = 1}^{n}

Γ ⊢ handle e with H : B! ε

C-Handle

The continuation in a clause is deep: invoking it resumes under the same handler. If a clause performs its own $ℓ_{i}$ , its output row $ε$ contains $ℓ_{i}$ . The premise for the handled computation then contains two copies.

Referenced from 2 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Here is the calculation for exceptions. Fix a result type $B$ , a fallback $d : B$ , and a row $ν$ . Define $\begin{aligned} C_{d}^{B} = & {return x \mapsto return x; raise (p; k) \mapsto return d}, \\ R^{B} = & {return x \mapsto return x; raise (p; k) \mapsto perform raise p to z . k z} . \end{aligned}$ The fallback handler has output row $ν$ . Its operation-clause premise is $d : B, p : Error, k : 0 \overset{ν}{\to} B ⊢ return d : B! ν .$ Consequently, if $e : B! ⟨ raise ∣ ν ⟩$ , then $handle e with C_{d}^{B} : B! ν$ .

The rethrower has output row $ε = ⟨ raise ∣ ν ⟩$ . Its operation clause uses the empty response only after the re-performed request: $\frac{\begin{matrix} \frac{\begin{matrix} Σ (raise) = Error ⇝ 0 \\ p : Error, k : 0 \overset{ε}{\to} B ⊢_{v} p : Error \end{matrix}}{p : Error, k : 0 \overset{ε}{\to} B ⊢ perform raise p : 0! ε} C - Op \\ p : Error, z : 0, k : 0 \overset{ε}{\to} B ⊢ k z : B! ε \end{matrix}}{p : Error, k : 0 \overset{ε}{\to} B ⊢ perform raise p to z . k z : B! ε} C - To .$ Thus $R^{B}$ has input row $⟨ raise, raise ∣ ν ⟩$ and output row $⟨ raise ∣ ν ⟩$ . No value of $0$ has been invented: $z$ is bound by the sequencing form, and the continuation call lies after the re-performed request. The fallback trace below discards that continuation instead of manufacturing a response.

This typing predicts the reduction. For a handler-free request context $R$ , put $q = R [perform raise p]$ , and assume $q : B! ⟨ raise, raise ∣ ν ⟩$ . Rule C-Op may choose any tail; here its tail already contains one $raise$ , while the displayed request contributes the other. The inner handler consumes the displayed occurrence and its clause re-performs the one that remains visible. The inner handler rethrows outside itself: $\begin{aligned} handle q with R^{B} & ⟶ perform raise p to z . \\ (λ y . handle R [return y] with R^{B}) z . \end{aligned}$ An outer fallback handler captures this request. Its clause discards the rebuilt continuation, so $handle (handle q with R^{B}) with C_{d}^{B} ⟶^{2} return d .$ At the type level the two handlers remove the two occurrences in succession: $B! ⟨ raise, raise ∣ ν ⟩ \overset{R^{B}}{\to} B! ⟨ raise ∣ ν ⟩ \overset{C_{d}^{B}}{\to} B! ν .$

A logging rethrower prefixes the clause of $R^{B}$ by $perform \log p to u$ . With $ε_{L} = ⟨ \log, raise ∣ ν ⟩$ , both operations and the continuation call have effect $ε_{L}$ , modulo exchange. Its input is therefore $⟨ raise, \log, raise ∣ ν ⟩$ , and its output is $ε_{L}$ . Applied to the transaction, the tail in $E_{μ}$ is instantiated to provide the second $raise$ and the $\log$ ; $get$ and $put$ remain in the ambient tail throughout. More explicitly, put $E_{ξ}^{L} = ⟨ get, put, \log, raise ∣ ξ ⟩ .$ The logging rethrower takes $Int! ⟨ raise ∣ E_{ξ}^{L} ⟩$ to $Int! E_{ξ}^{L}$ , while the required instance of the transaction is obtained from $E_{μ}$ by the row calculation $\begin{aligned} E_{μ} [⟨ \log, raise ∣ ξ ⟩ / μ] & \overset{(25.1)}{\equiv} ⟨ get, put, raise, \log, raise ∣ ξ ⟩ \\ \overset{(25.4)}{\equiv} ⟨ raise ∣ get, put, \log, raise ∣ ξ ⟩ \\ \equiv ⟨ raise ∣ E_{ξ}^{L} ⟩ . \end{aligned}$ The handler removes the first displayed occurrence and leaves exactly $E_{ξ}^{L}$ . Equivalently, within $ε_{L}$ take $ν = ⟨ get, put ∣ ξ ⟩$ .

Exercise 25.2 — Typing the two catches ¶

★★☆ Instantiate the displays above with $B = Int$ and $ν = ⟨ get, put ∣ ξ ⟩$ . Write both complete instances of C-Handle, including the return-clause premises, and display the effect before and after each handler.

Referenced from 3 locations

Operational meaning

Definition 25.5 — Operational semantics ¶

Evaluation contexts and handler-free request contexts are generated by $\begin{aligned} E & ::= [] ∣ E to x . e ∣ let x = E in e \\ ∣ handle E with H, \\ R & ::= [] ∣ R to x . e ∣ let x = R in e . \end{aligned}$ A $let$ -shaped request context is included so the context grammar is closed under the term syntax. It is unreachable in a well-typed terminal request: C-Let requires its bound computation to have the empty row, so that position cannot expose an operation. A request context $R$ contains no handler frame. Consequently the handler displayed at a root is the nearest syntactic handler around the request: it either handles that label or forwards the request across exactly one handler layer. The same grammar also describes a terminal request context when no handler encloses it. Besides beta and sequencing, the roots are $\begin{aligned} (λ x . e) v & ⇝_{0} e [v / x], \\ (return v) to x . e & ⇝_{0} e [v / x], \\ let x = return v in e & ⇝_{0} e [v / x], \\ handle (return v) with H & ⇝_{0} e_{r} [v / x], \\ handle R [perform ℓ_{i} v] with H & ⇝_{0} e_{i} [v / p_{i}, \\ (λ y . handle R [return y] with H) / k_{i}] . \end{aligned}$ If $ℓ$ is not handled by $H$ , forwarding preserves the operation and rebuilds its continuation: $\begin{aligned} handle R [perform ℓ v] with H \\ ⇝_{0} perform ℓ v to y . handle R [return y] with H . \end{aligned}$ The last root in the first display is H-Op; the forwarding root is H-Forward. The reduction relation is the least relation containing these roots and closed under $E$ . Their label tests are complementary. Because $R$ has no handler frame, a nested request first meets its innermost handler; context closure cannot also contract an outer handler root. Repeated H-Forward steps give the familiar derived “open context” behavior, but that multi-layer behavior is not a primitive reduction.

Referenced from 2 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

The active spine of $E$ is the ordered list of frames encountered from its hole to its root.

Lemma 25.6 — Nearest-handler decomposition ¶

For every evaluation context $E$ , request label $ℓ$ , and value $v$ , exactly one of the following decompositions applies:

$E [perform ℓ v] = R [perform ℓ v]$ for a unique request context $R$ ;
there are unique $E^{'}$ , $R$ , and $H$ such that $E [perform ℓ v] = E^{'} [handle R [perform ℓ v] with H],$ and the displayed occurrence of $H$ is the innermost handler frame on the active spine.

In the second case, membership of $ℓ$ in $handled (H)$ selects exactly one of H-Op and H-Forward.

Referenced from 6 locations

Proof of Lemma 25.6 — Nearest-handler decomposition

Proof. Read the frames of $E$ from the hole outward. If there is no handler frame, all frames belong to the grammar of $R$ , giving the first decomposition. Otherwise split the frame list immediately after its first handler. The inner prefix is the unique $R$ , that first handler is the unique $H$ , and the remaining suffix is the unique $E^{'}$ . The two cases are disjoint by the presence or absence of a handler frame, and the two label tests are complementary. ◻

Exercise 25.3 — Forward exactly one layer ¶

★★☆ Let $R$ be handler free, let $ℓ \notin handled (H_{0})$ , and let $H_{1}$ contain the clause $ℓ (p; k) \mapsto e_{ℓ}$ . Starting from $handle (handle R [perform ℓ v] with H_{0}) with H_{1},$ write the H-Forward step through $H_{0}$ and the next H-Op step at $H_{1}$ , including both rebuilt continuations. Give the decomposition from Lemma 25.6 before each step, and explain syntactically why the outer H-Op is not a root of the initial term.

Referenced from 4 locations

Lemma 25.7 — Replacement for request contexts ¶

Suppose $Γ ⊢ R [e] : B! ε$ , and the derivation assigns $Γ ⊢ e : A! δ$ at the hole. If $Γ ⊢ e^{'} : A! δ$ , then $Γ ⊢ R [e^{'}] : B! ε$ .

Referenced from 4 locations

Proof of Lemma 25.7 — Replacement for request contexts

Proof. Induct on $R$ . A sequencing frame uses the induction hypothesis in the left premise of C-To; the right premise is unchanged. A let frame uses it in the first premise of C-Let. Sequencing and let are exactly the two constructors of a request context. ◻

Write $σ^{'} ⊒ σ$ when every kind-correct instance of $σ$ is an instance of $σ^{'}$ , read “ $σ^{'}$ is at least as general as $σ$ ” exactly as in chapter 3.

Lemma 31.8 — Type-and-row action and scheme enlargement ¶

If $Γ ⊢ J$ is a value or computation judgment and $S$ is kind preserving, then $S Γ ⊢ S J$ , after renaming scheme binders away from $dom (S)$ . If $σ^{'} ⊒ σ$ , replacing an assumption $y : σ$ by $y : σ^{'}$ preserves a derivation.

Referenced from 5 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Lemma 31.8 — Type-and-row action and scheme enlargement

Proof. Induct on the derivation. The variable case composes the selected instance with $S$ ; the constant case does the same within its closed declaration; C-Op is unchanged because every $P_{ℓ}, R_{ℓ}$ is closed; and C-RowConv uses the fact that kind-preserving substitution preserves $\equiv$ . In C-Let, the variables later bound by generalization are still free in the bound monotype. Apply one finite kind-preserving bijection to the entire bound-expression premise and to the body’s generalized declaration. This is licensed because those variables are fresh for $Γ$ , and it makes them fresh for both the domain and range variables of $S$ ; it is not merely an alpha-renaming of the scheme prefix. The scheme recomputed from $S Γ, S A_{1}$ is at least as general as the pointwise image of the old scheme. Put $Q = ftv (A_{1}) ∖ ftv (Γ)$ and choose the variables of $Q$ fresh for the domain and range of $S$ . Then $S$ fixes every member of $Q$ , none occurs in $S Γ$ , and $Q \subseteq ftv (S A_{1}) ∖ ftv (S Γ) .$ Thus every instance of $S (\forall Q . A_{1})$ is an instance of $gen (S Γ, S A_{1})$ . Scheme enlargement therefore derives the body premise from its old instance. The handler case applies the induction hypotheses under the renamed return, parameter, and resumption binders. All binders are renamed fresh before an induction hypothesis is used. Scheme enlargement itself changes only V-Var: an instance admitted by $σ$ is still admitted by $σ^{'}$ . ◻

Lemma 25.8 — Type, row, ordinary, and generalized substitution ¶

If $Γ, x : A, Δ ⊢_{v} w : B$ and $Γ ⊢_{v} v : A$ , then $Γ, Δ ⊢_{v} w [v / x] : B$ . If $Γ, x : A, Δ ⊢ e : B! ε$ , then $Γ, Δ ⊢ e [v / x] : B! ε$ .

Referenced from 5 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Lemma 25.8 — Type, row, ordinary, and generalized substitution

Proof. Use a simultaneous induction on value and computation typing. At V-Var, the distinguished variable uses the premise for $v$ , while every other variable is unchanged. In V-Const, the declared instance is unchanged. In V-Lam, rename the lambda binder away from $x$ and the free variables of $v$ , then apply the computation induction hypothesis below it. C-Return, C-App, and C-To apply the appropriate hypotheses to their immediate subderivations. In C-Op, substitute in the parameter value; the closed declaration types remain literally $P_{ℓ}, R_{ℓ}$ . The C-RowConv case reapplies the same row equivalence.

For C-Let, rename its binder $y$ away from $x, v$ . The induction hypothesis types the substituted bound computation. Removing $x : A$ from the surrounding context can only enlarge $ftv (A_{1}) ∖ ftv (Γ)$ . Hence the new scheme $σ_{1}^{'}$ computed by C-Let is at least as general as the old $σ_{1}$ : $σ_{1}^{'} ⊒ σ_{1}$ . Scheme enlargement retags the body derivation with $y : σ_{1}^{'}$ , and its induction hypothesis substitutes for $x$ . In C-Handle, alpha-rename the return binder and every parameter and resumption binder $p_{i}, k_{i}$ . Apply the induction hypotheses to the body, the return clause under its value binder, and every operation clause under both its parameter value binder and its resumption value binder. Their arrow and row annotations are unchanged, so C-Handle reconstructs the conclusion. ◻

Lemma 31.10 — Generalized value substitution ¶

If $\bar{a} \cap ftv (Γ) = \emptyset$ , $Γ ⊢_{v} v : A$ , and $Γ, x : \forall \bar{a} . A, Δ ⊢ J$ , then $Γ, Δ ⊢ J [v / x]$ . Each occurrence of $x$ may choose a different kind-correct type-and-row instance of $\bar{a}$ .

Referenced from 3 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Lemma 31.10 — Generalized value substitution

Proof. Repeat the simultaneous induction of lemma 25.8. Its only new variable case is an occurrence of $x$ at an instantiation $T A$ . Freshness gives $T Γ = Γ$ , so lemma 31.8 derives $Γ ⊢_{v} v : T A$ . Lambda, operation, conversion, let-scheme, return, parameter, and resumption binders use exactly the cases just enumerated. Thus separate occurrences may instantiate $\bar{a}$ differently without changing the substituted term. ◻

Lemma 31.11 — Arrow canonical form ¶

If $\cdot ⊢_{v} v : A \overset{ε}{\to} B$ , then $v = λ x . e$ for some $x, e$ .

Referenced from 3 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Lemma 31.11 — Arrow canonical form

Proof. Invert value typing. The empty context excludes V-Var, and every V-Const instance has the outer constructor of its closed base declaration. Only V-Lam concludes an arrow type. ◻

Theorem 25.9 — Preservation ¶

If $Γ ⊢ e : A! ε$ and $e ⟶ e^{'}$ , then $Γ ⊢ e^{'} : A! ε$ .

Referenced from 3 locations

Proof of Theorem 25.9 — Preservation

Proof. The beta and sequencing roots use ordinary substitution from lemma 25.8. For the let root, inversion of its pure-return premise gives $Γ ⊢_{v} v : A$ , and the variables generalized by C-Let are fresh for $Γ$ ; use lemma 31.10. A handled return uses ordinary substitution in the return clause.

For a handled operation, invert the typing of the request context. Its hole has type $R_{i}! δ$ . Rule C-Return assigns the same hole effect to $return y$ ; lemma 25.7 reconstructs the handler premise, and C-Handle gives the captured continuation type $R_{i} \overset{ε}{\to} B$ . First substitute the request parameter $v : P_{i}$ for the clause’s value binder $p_{i}$ ; then substitute the rebuilt continuation value for its resumption binder $k_{i}$ . Lemma 25.8 gives both steps, including any nested lambdas, lets, operations, handlers, or row conversions in the clause.

For forwarding, inversion gives $⟨ ℓ_{1}, \dots, ℓ_{n} ∣ ε ⟩ \equiv ⟨ ℓ ∣ δ ⟩, ℓ \notin {ℓ_{1}, \dots, ℓ_{n}} .$ Lemma 25.2 yields $ε \equiv ⟨ ℓ ∣ ε^{'} ⟩$ . Replacement types the rebuilt continuation at $ε$ , and C-Op followed by C-To types H-Forward at the same effect. Contextual cases apply the induction hypothesis to the active premise; C-RowConv reapplies its unchanged equivalence. ◻

An exposed terminal request is $R [perform ℓ v]$ . It contains no handler frame: a request immediately inside a handler either takes H-Op or takes H-Forward, while a more deeply nested request first reduces at its innermost handler. Thus an exposed terminal request is an observable request, not a runtime fault and not a reducible forwarding configuration.

Theorem 25.10 — Progress and absence of unhandled operations ¶

If $\cdot ⊢ e : A! ε$ , then exactly one of the following holds: $e = return v$ , the computation takes a step, or it is an exposed terminal request whose label occurs in $ε$ . Hence a closed computation of effect $⟨ ⟩$ cannot expose an operation.

Referenced from 4 locations

Proof of Theorem 25.10 — Progress and absence of unhandled operations

Proof. Induct on typing. Lemma 31.11 settles application. For sequencing, apply the induction hypothesis to the first computation: a return takes the sequencing step, a reduction lifts, and an exposed operation remains exposed in the enlarged terminal request context. The let case is similar, except that its first computation has empty effect: an exposed-operation outcome is impossible, a return takes the let step, and a reduction lifts through the let frame. For a handler, a returned value uses its return rule; a reduction lifts; a request for a handled label uses H-Op; and every other request uses H-Forward. It is therefore a step rather than a terminal-request outcome. For C-RowConv, apply the induction hypothesis to its premise. A return or reduction is unchanged. In the exposed-request alternative, row equivalence preserves every label multiplicity, so occurrence of the exposed label in the premise row implies its occurrence in the converted row. Inversion of C-Op and repeated cancellation show that the exposed label occurs in the concluding row. The empty row has multiplicity zero for every label. Finally, the three outcomes are disjoint: returns and terminal requests have different outer forms, and a terminal request has no redex. For a step, the handler-free grammar of $R$ and the ordinary call-by-value forms give unique active decompositions. In the request case lemma 25.6 gives the unique nearest root, where the handled-label test selects exactly one of H-Op and H-Forward. ◻

Exercise 25.4 — The forwarding case ¶

★★☆ Fill in the forwarding case of preservation without writing “by weakening.” Name the row equivalence obtained by inversion, apply the second part of lemma 25.2, and derive the type of the continuation rebuilt in H-Forward.

Referenced from 3 locations

Unification by exposure

The ordinary first-order unification clauses handle type variables, constants, and arrows. The row clause exposes a requested label at the head and returns a most-general substitution.

Write $rewrite (ε, ℓ) = (S, ε^{'})$ when the operation succeeds. Its contract is $\begin{matrix} (31.5) & S ε \equiv ⟨ ℓ ∣ S ε^{'} ⟩ . \end{matrix}$ This is the constrained insertion operation of chapter 4 with its lacks premise removed: both operations expose one requested label and return the residue, but duplicate effect labels make absence evidence unnecessary here. It is defined by the following equations. In Rw-Var, choose $ν$ outside the row variables in the entire unification problem and every substitution constructed so far. $\begin{matrix} (31.6) & \begin{aligned} rewrite (⟨ ℓ ∣ ε ⟩, ℓ) & = (id, ε) & R w - H e a d \\ rewrite (⟨ ℓ^{'} ∣ ε ⟩, ℓ) & = (S, ⟨ ℓ^{'} ∣ ε^{'} ⟩) & R w - S k i p \\ ℓ^{'} \neq ℓ, rewrite (ε, ℓ) = (S, ε^{'}), \\ rewrite (μ, ℓ) & = ([μ \mapsto ⟨ ℓ ∣ ν ⟩], ν) & R w - V a r . \end{aligned} \end{matrix}$ Rewriting the empty row fails. In Rw-Skip, the returned substitution also acts on the residual row.

The unifier state is a list of pending equations and an accumulated substitution. Write $U (A, B)$ for the result from initial state $([A ≐ B], id)$ . After a clause returns $S_{1}$ , every residual equation is replaced by its $S_{1}$ -image before the work list continues; the arrow and row-extension displays spell out those states.

The unifier tries cases in the fixed order used by definition 25.11: reflexivity, variable orientation, empty and constructor clauses, and only then row extension. Hence the following clause does not compete with U-Var. Let $tail (ε)$ be the final row variable, when one exists. The row-extension clause of unification is $\begin{matrix} (31.7) & \begin{array}{l} U (⟨ ℓ ∣ ε_{1} ⟩, ε_{2}) : \\ (S_{1}, ε_{3}) := rewrite (ε_{2}, ℓ); \\ if tail (ε_{1}) \in dom (S_{1}) then fail; \\ S_{2} := U (S_{1} ε_{1}, S_{1} ε_{3}); \\ return S_{2} \circ S_{1} . \end{array} \end{matrix}$ The membership test is false when the left row has no variable tail.

Definition 25.11 — All unification cases ¶

Unification is called only on two objects of the same kind and preserves that kind. Its type objects are exactly $α$ , $b$ , and $A \overset{ε}{\to} B$ ; its row objects are exactly $μ$ , $⟨ ⟩$ , and $⟨ ℓ ∣ ε ⟩$ . In the following display, $a$ ranges over variables of either kind, $X$ over an object of that same kind, and $b$ over base types: $\begin{matrix} (31.8) & \begin{array}{rcll} U (a, a) & = & id & U - R e f l \\ U (a, X) & = & [a \mapsto X] & U - V a r, a \notin ftv (X), a \neq X \\ U (X, a) & = & U (a, X) & U - S y m, X is not a variable \\ U (b, b) & = & id & U - B a s e \\ U (⟨ ⟩, ⟨ ⟩) & = & id & U - E m p t y . \end{array} \end{matrix}$ Rule U-Var fails its occurs check when $a \in ftv (X)$ . After reflexivity and the variable clauses, the complete same-kind clash table is $\begin{matrix} (31.8 a) & \begin{array}{rcll} U (b, b^{'}) & = & fail & U - C l a s h - B a s e, b \neq b^{'} \\ U (b, A \overset{ε}{\to} B) & = & fail & U - C l a s h - B a s e A r r o w \\ U (A \overset{ε}{\to} B, b) & = & fail & U - C l a s h - A r r o w B a s e \\ U (⟨ ⟩, ⟨ ℓ ∣ ε ⟩) & = & fail & U - C l a s h - E m p t y E x t e n d \\ U (⟨ ℓ ∣ ε ⟩, ⟨ ⟩) & = & fail & U - C l a s h - E x t e n d E m p t y . \end{array} \end{matrix}$ A proposed type–row equation is rejected as ill kinded before $U$ is called; it is not another same-kind clash case.

For arrows, the complete clause is $\begin{matrix} (31.9) & \begin{array}{l} S_{1} := U (A_{1}, A_{2}); \\ S_{2} := U (S_{1} ε_{1}, S_{1} ε_{2}); \\ S_{3} := U (S_{2} S_{1} B_{1}, S_{2} S_{1} B_{2}); \\ U (A_{1} \overset{ε_{1}}{\to} B_{1}, A_{2} \overset{ε_{2}}{\to} B_{2}) := S_{3} S_{2} S_{1} . U - A r r o w \end{array} \end{matrix}$ Rows headed by a label use (25.7), called U-Extend; a variable or empty row on either side has already been covered by U-Refl, U-Var, U-Sym, U-Empty, or one of the five displayed U-Clash cases. These cases are disjoint after trying reflexivity and variable binding first, so the displays define the whole algorithm at both kinds.

Referenced from 4 locations

The guard in (25.7) is load bearing. Without it, unifying $\begin{matrix} (31.10) & ⟨ ℓ_{1} ∣ μ ⟩ with ⟨ ℓ_{2} ∣ μ ⟩, ℓ_{1} \neq ℓ_{2} . \end{matrix}$ first exposes $ℓ_{1}$ on the right by proposing $S_{1} = [μ \mapsto ⟨ ℓ_{1} ∣ μ_{1} ⟩], ε_{3} = ⟨ ℓ_{2} ∣ μ_{1} ⟩, ⟨ ℓ_{1} ∣ μ_{1} ⟩ ≐ ⟨ ℓ_{2} ∣ μ_{1} ⟩ .$ The recursive equation is (25.10) again with fresh tail $μ_{1}$ . Each round consumes one tail variable and produces the next, so the substitution grows without bound. With the guard the original equation fails. It has no finite-row solution: cancelling the common multiset denoted by $μ$ would assert ${ℓ_{1}} = {ℓ_{2}}$ .

Lemma 25.12 — Exposure ¶

If $rewrite (ε, ℓ) = (S, ε^{'})$ , then (25.5) holds. Moreover, if $T ε \equiv ⟨ ℓ ∣ δ ⟩$ , then rewriting succeeds and, for every finite protected set $Z$ of variables, its fresh $ν$ may be chosen outside $Z$ and there is a substitution $Q$ such that $\begin{matrix} (31.11) & Q agrees with T on Z, T = Q \circ S on Z \cup ftv (ε), δ \equiv Q ε^{'} . \end{matrix}$ Thus exposure is most general.

Referenced from 6 locations

Proof of Lemma 25.12 — Exposure

Proof. For soundness, induct on (25.6). The head case is reflexivity. The skip case applies the induction hypothesis below the skipped label and then exchanges $ℓ$ past $ℓ^{'}$ . In the variable case, substitution gives $⟨ ℓ ∣ ν ⟩$ directly.

For factorization, induct down the visible prefix of $ε$ . If its head is $ℓ$ , cancel it and take the identity factor. If $ε = ⟨ ℓ^{'} ∣ ε_{1} ⟩$ with $ℓ^{'} \neq ℓ$ , the recursive rewrite returns $ε_{1}^{'}$ , and the second clause of lemma 25.2 gives $T ε_{1} \equiv ⟨ ℓ ∣ δ^{'} ⟩$ ; its first clause then gives $δ \equiv ⟨ ℓ^{'} ∣ δ^{'} ⟩$ . The induction hypothesis gives $δ^{'} \equiv Q ε_{1}^{'}$ , and congruence restores the skipped $ℓ^{'}$ . If the tail is $μ$ , the assumed equivalence says that $T μ$ contains $ℓ$ ; exchange that occurrence to the head and write $T μ \equiv ⟨ ℓ ∣ ρ ⟩$ . Choose $ν \notin Z$ , define $Q ν = ρ$ , and put $Q α = T α$ for every $α \neq ν$ . Then $T = Q \circ [μ \mapsto ⟨ ℓ ∣ ν ⟩]$ on $Z \cup ftv (ε)$ , and $Q$ agrees with $T$ on $Z$ . The empty case contradicts the assumed positive $ℓ$ -multiplicity. ◻

Lemma 25.13 — Termination ¶

Both $rewrite$ and $U$ terminate on finite types and finite rows.

Referenced from 3 locations

Proof of Lemma 25.13 — Termination

Proof. Rewriting either stops or calls itself on a proper row tail. For a row $ε$ , let $| ε |$ be the number of visible label constructors; a variable or empty tail contributes zero. Consider the recursive call made by (25.7). If rewriting finds $ℓ$ in the visible prefix of the right row, that call has removed the left head and the exposed right occurrence. The sum of the two visible sizes decreases by two.

Otherwise the right row is $⟨ L ∣ μ ⟩$ , where $L$ has no $ℓ$ , and Rw-Var binds $μ \mapsto ⟨ ℓ ∣ ν ⟩$ . The guard says that $μ$ is not the tail of $ε_{1}$ ; since a row has only one tail, $μ$ does not occur in $ε_{1}$ . If $| ε_{1} | = m$ and $| L | = n$ , the old extension equation has visible size $1 + m + n$ , while its recursive tail equation has size $m + n$ . Thus every recursive row-extension call strictly decreases a natural number. Variable, empty, and equal-head cases either stop or enter that decreasing call; both empty–extension clash orientations stop immediately. Thus row unification terminates.

The recursive U-Arrow presentation and the work-list presentation agree: its three recursive calls push the domain, effect, and codomain equations in that order, composing each returned substitution into the remaining list. For that work-list representation, let $C$ be the finite list of equations remaining after applying the accumulated substitution. Let $v (C)$ count distinct unsolved variables of either kind, let $c (C)$ count all base and arrow constructors occurring in the equations, and let $n (C)$ count equations. Use the lexicographic measure $\begin{matrix} (31.12) & M (C) = (v (C), c (C), n (C)) \in N^{3} . \end{matrix}$ Rows contain no base or arrow constructors. A binding of a row variable therefore cannot duplicate anything counted by $c (C)$ ; it changes only the row-specific measure handled by the atomic row procedure. A U-Var step permanently removes its variable and introduces no fresh outer-work-list variable, so the first component decreases even if applying the binding duplicates constructors. A U-Arrow step keeps the first component fixed and removes the two arrow heads. Its domain, effect, and codomain constructors already occurred below those heads, so the second component decreases. A successful U-Base step also decreases the second component. A U-Refl step removes an equation. Each base–base or base–arrow clash stops immediately. A row-unification call is the terminating atomic procedure proved above. Every fresh tail introduced by exposure replaces one bound old tail, so this call does not increase $v$ ; if $v$ stays fixed, removing the solved row equation without adding an outer equation decreases $n$ . Thus every outer transition decreases $M$ , and the complete unifier terminates. ◻

Theorem 25.14 — Most-general type-and-row unification ¶

If $U (A, B) = S$ , then $S A \equiv S B$ . Conversely, if $T A \equiv T B$ , the algorithm succeeds with some $S$ , and there is a $Q$ such that $T = Q \circ S$ on the variables of $A, B$ .

Referenced from 4 locations

Proof of Theorem 25.14 — Most-general type-and-row unification

Proof. Soundness is by induction on a successful unifier derivation; the five clash cases have no successful conclusion. If a variable $α$ is bound to $B$ , the occurs check has established $α \notin ftv (B)$ , and the returned substitution makes both sides literally $B$ . Equal constants return the identity. For arrows, the domain hypothesis equates the domains; the effect hypothesis equates the two effects after that substitution; and the codomain hypothesis equates the codomains after both earlier substitutions. Congruence then equates the arrows. For (25.7), Lemma 25.12 gives $S_{1} ε_{2} \equiv ⟨ ℓ ∣ S_{1} ε_{3} ⟩;$ the recursive hypothesis equates the tails after $S_{2}$ , so congruence equates the original rows after $S_{2} S_{1}$ .

For completeness, strengthen the induction statement to factorization. In a variable equation $α ≐ B$ , any unifier $T$ satisfies $T α = T B$ . Define $Q$ to agree with $T$ away from $α$ ; then $T = Q \circ [α \mapsto B]$ on the variables of the equation. If $α \in ftv (B)$ and $B \neq α$ , substitution gives an equation in which $T α$ contains itself beneath at least one constructor. Exchange preserves the number of row-extension constructors, and type congruence preserves all other constructor counts, so this equation would imply $| T α | \geq 1 + | T α |$ , impossible for a finite type. Thus no unifier exists. The constant case is reflexive. Distinct bases cannot be unified; a base and an arrow have different outer type constructors; and an empty row cannot equal an extension because their multiplicities are respectively zero everywhere and positive at the head label. These arguments cover both displayed orientations, so every same-kind U-Clash failure is complete. A type–row pair is not a well-kinded equation. For arrows, factor the given unifier through the domain MGU, apply the residual factor to the substituted effect equation, and then to the substituted codomain equation. The three induction hypotheses compose in exactly that order.

In the extension case, apply the factorization half of lemma 25.12 to the occurrence of $ℓ$ on the right, taking $Z = ftv (ε_{1})$ . The protected-set clause produces $T = Q_{1} S_{1}$ on every variable of the left row and reduces the remaining equality to $Q_{1} S_{1} ε_{1} \equiv Q_{1} S_{1} ε_{3}$ . The induction hypothesis gives $Q_{1} = Q_{2} S_{2}$ , hence $T = Q_{2} S_{2} S_{1}$ .

For the guard, suppose it fires while unifying $⟨ ℓ, L ∣ μ ⟩$ with $⟨ M ∣ μ ⟩$ . Rewriting reached the shared tail $μ$ , so no label in the finite prefix $M$ is $ℓ$ . If a finite substitution $T$ unified the rows, equality of multiplicities would give ${ℓ} + M (L) + M (T μ) = M (M) + M (T μ) .$ Cancel the common multiset $M (T μ)$ . The multiplicity of $ℓ$ on the left is $1 + M (L) (ℓ) > 0$ , while it is zero on the right, a contradiction. Thus the guard discards no unifier; (25.10) is its smallest instance. Remaining failures are constructor conflicts, empty-row exposure, or the occurs check, each incompatible with a finite unifier. ◻

Exercise 25.5 — Trace the guard ¶

★★☆ Trace (25.6)– (25.7) on (25.10), naming the fresh variable and the substitution returned by rewriting. Identify the exact guard test that fails. Then trace $⟨ ℓ_{1} ∣ μ ⟩$ against $⟨ ℓ_{2}, ℓ_{1} ∣ ν ⟩$ and give its MGU.

Referenced from 3 locations

Exercise 25.6 — Duplicate labels unify ¶

★★☆ Compute an MGU of $⟨ raise, get ∣ μ ⟩ and ⟨ get, raise, raise ∣ ν ⟩ .$ State the residual equation and show explicitly how every other unifier factors through yours.

Referenced from 3 locations

Algorithm W with effects

Algorithm W gains a second variable sort and clauses for operation requests, handlers, and row equations. Variable instantiation, lambda, application, and let-generalization keep their Hindley–Milner form.

Definition 25.15 — Algorithm W with effects ¶

Write $W_{v} (Γ, v) = (S, τ), W_{c} (Γ, e) = (S, τ, ε) .$ Fresh variables are drawn from one monotonically consumed supply. Thus each choice is distinct from every variable in the environment or term, in the domain or range of a substitution already constructed, and in every type or row returned by an earlier recursive call. A recursive call receives the unused tail of the supply; this state parameter is implicit in the displayed $W$ notation. Substitutions act on the remaining environment before that call. We maintain the invariant that the reported type and row are fixed by the reported substitution; every tuple below is written after applying the substitutions accumulated at that point.

For values:

A variable instantiates every quantified type and row variable in its scheme with a fresh variable and returns the identity substitution.
If $C (c) = \forall \bar{α} \bar{μ} . τ$ , a constant replaces every displayed quantifier by a fresh variable, obtaining $T τ$ , and returns $(id, T τ)$ .
For $λ x . e$ , choose fresh $α$ , compute $W_{c} (Γ, x : α, e) = (S, τ, ε)$ , and return $(S, S α \overset{ε}{\to} τ)$ .

For computations:

For $return v$ , infer $(S, τ)$ for $v$ , choose a fresh row variable $μ$ , and return $(S, τ, μ)$ . A fresh open row is principal because C-Return admits every effect.
For $v_{1} v_{2}$ , compute $(S_{1}, τ_{1}) = W_{v} (Γ, v_{1}), (S_{2}, τ_{2}) = W_{v} (S_{1} Γ, v_{2}) .$ Choose fresh $α, μ$ .

Let $S_{3} = U (S_{2} τ_{1}, τ_{2} \overset{μ}{\to} α)$ . The answer is $(S_{3} S_{2} S_{1}, S_{3} α, S_{3} μ)$ . The fresh application-row variable $μ$ is immediately unified with the latent row of the inferred function type; it is therefore absent from later worked traces unless that unification leaves it unconstrained.
For $e_{1} to x . e_{2}$ , compute $(S_{1}, τ_{1}, ε_{1})$ , then $(S_{2}, τ_{2}, ε_{2})$ under $S_{1} Γ, x : S_{1} τ_{1}$ . Let $S_{3} = U (S_{2} ε_{1}, ε_{2})$ . Return $(S_{3} S_{2} S_{1}, S_{3} τ_{2}, S_{3} ε_{2})$ .
For $perform ℓ v$ , compute $(S_{1}, τ) = W_{v} (Γ, v)$ , let $S_{2} = U (τ, P_{ℓ})$ , and choose fresh $μ$ . Return $(S_{2} S_{1}, R_{ℓ}, ⟨ ℓ ∣ μ ⟩) .$ The declaration types $P_{ℓ}, R_{ℓ}$ are closed, so applying any current substitution to them would be redundant.
For $let x = e_{1} in e_{2}$ , infer $(S_{1}, τ_{1}, ε_{1})$ , unify $ε_{1}$ with $⟨ ⟩$ , and call the result $S_{2}$ . Put $χ_{1} = {gen}_{c} (S_{2} S_{1} Γ, S_{2} τ_{1}! ⟨ ⟩) = \forall \bar{a} . (S_{2} τ_{1}! ⟨ ⟩), σ_{1} = \forall \bar{a} . S_{2} τ_{1}$ by quantifying variables free in the type-and-effect pair but not the environment. The computation scheme $χ_{1}$ records the pure effect for the soundness and principality statement; the term environment stores only its value-type projection $σ_{1}$ . Infer $(S_{3}, τ_{2}, ε_{2})$ for $e_{2}$ under $S_{2} S_{1} Γ, x : σ_{1}$ , and return $(S_{3} S_{2} S_{1}, τ_{2}, ε_{2})$ .
For $handle e with H$ , use the following accumulator. For an accumulated substitution $Q$ , define the oriented solve step $\begin{matrix} (31.13) & \begin{matrix} R = U (Q X, Q Y), \\ solve (Q; X ≐ Y) = R \circ Q . \end{matrix} \end{matrix}$ where the inferred object is always on the left and the expected object on the right. Choose fresh $β, μ$ , compute $(S_{0}, A_{0}, ε_{0}) = W_{c} (Γ, e)$ , and put $Q_{0} = S_{0}$ . For the return clause, compute $(S_{r}, B_{r}, δ_{r}) = W_{c} (Q_{0} Γ, x : Q_{0} A_{0}, e_{r}),$ then set $\begin{aligned} Q_{r}^{0} & = S_{r} Q_{0}, & Q_{r}^{1} & = solve (Q_{r}^{0}; B_{r} ≐ β), \\ Q_{r} & = solve (Q_{r}^{1}; δ_{r} ≐ μ) . \end{aligned}$ Starting with $Q_{0}^{c} = Q_{r}$ , process clauses in the fixed source order. The tempting resumption assumption $\begin{matrix} (b a d) & k_{i} : R_{i} \overset{Q_{i - 1}^{c} ε_{0}}{\to} Q_{i - 1}^{c} β \end{matrix}$ uses the handler input row. It is wrong: resuming reinstalls the handler, so a request already removed by the handler would be counted again. For a concrete counterexample, extend the operation signature by $Σ (ask) = 1 ⇝ Env$ . For a one-clause $ask$ handler with input $⟨ ask ∣ μ ⟩$ and output $μ$ , the bad type gives $k_{i} ()$ an extra $ask$ ; the clause can no longer satisfy its required output $μ$ . The resumption therefore has type $R_{i} \overset{Q_{i - 1}^{c} μ}{\to} Q_{i - 1}^{c} β$ , using the accumulated output row. At clause $i$ , compute $\begin{aligned} (S_{i}, B_{i}, δ_{i}) = W_{c} ( & Q_{i - 1}^{c} Γ, \\ p_{i} : P_{i}, \\ k_{i} : R_{i} \overset{Q_{i - 1}^{c} μ}{\to} Q_{i - 1}^{c} β; e_{i}) . \end{aligned}$ Again $P_{i}$ and $R_{i}$ are closed declarations; only the inferred output type and row require the accumulated substitution. The semicolon separates the extended context from the clause term. Put $\begin{aligned} Q_{i}^{0} & = S_{i} Q_{i - 1}^{c}, \\ Q_{i}^{1} & = solve (Q_{i}^{0}; B_{i} ≐ β), \\ Q_{i}^{c} & = solve (Q_{i}^{1}; δ_{i} ≐ μ) . \end{aligned}$ Finally set $\begin{matrix} (31.14) & Q^{'} = solve (Q_{n}^{c}; ε_{0} ≐ ⟨ ℓ_{1}, \dots, ℓ_{n} ∣ μ ⟩) . \end{matrix}$ Return $(Q^{'}, Q^{'} β, Q^{'} μ)$ .

Every recursive call is on a proper subterm, and every equation goes to the terminating unifier. The fixed source order is part of this algorithm. We do not claim a separate clause-order-independence theorem; principality is proved for this stated order below.

Referenced from 2 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Lemma 25.16 — Computation and pure-let generalization ¶

Let $Γ ⊢ e : A! ε$ , and put $χ = {gen}_{c} (Γ, A! ε)$ . Every instance of the pair $A! ε$ that leaves $Γ$ fixed is an instance of $χ$ , and $χ$ is most general with this property. If $ε = ⟨ ⟩$ , deleting the fixed empty effect from $χ$ gives ${gen}_{v} (Γ, A)$ , the most-general value scheme admitted by C-Let.

Referenced from 6 locations

Proof of Lemma 25.16 — Computation and pure-let generalization

Proof. Partition the free variables of $A! ε$ into those free in $Γ$ and the remainder. A substitution that leaves $Γ$ fixed cannot quantify or rename the first part; its action on the remainder is precisely an instantiation of the variables quantified by ${gen}_{c}$ . The identity instantiation recovers the pair, and any other scheme whose instances are exactly the $Γ$ -fixing instances must quantify only variables in the same remainder. Its instances therefore factor through $χ$ . When the row is empty, it contributes no free row variables, so the quantified list is exactly the one in ${gen}_{v} (Γ, A)$ . Purity permits the returned value to be used repeatedly without duplicating an operation. ◻

Theorem 25.17 — Soundness of inference ¶

If $W_{v} (Γ, v) = (S, A)$ , then $S Γ ⊢_{v} v : A$ . If $W_{c} (Γ, e) = (S, A, ε)$ , then $S Γ ⊢ e : A! ε$ .

Referenced from 3 locations

Proof of Theorem 25.17 — Soundness of inference

Proof. Proceed by simultaneous induction on values and computations. A variable is typed by V-Var at the fresh instance selected by W; a constant is typed by V-Const at the corresponding fresh instance of its closed declared scheme. For a lambda, the computation induction hypothesis types the body under $S Γ, x : S α$ , so V-Lam gives precisely W’s arrow.

At every sequential inference stage, maintain this invariant: after the accumulator is $Q_{j}$ , lemma 31.8 transports every judgment inferred through stage $j$ to context $Q_{j} Γ$ and applies $Q_{j}$ to its reported type and row. Each new MGU is composed only after this transport.

For a return, the value hypothesis derives $S Γ ⊢_{v} v : A$ , and C-Return permits W’s fresh $μ$ . In an application, lemma 31.8 transports both value hypotheses through the substitutions returned by the later calls, so they type the operator and operand after the accumulated substitution. Unifier soundness changes the operator type to $τ_{2} \overset{μ}{\to} α$ ; C-App gives the reported result and effect. The operation case is the same calculation against the fixed parameter type $P_{ℓ}$ , followed by C-Op. For sequencing, the two computation hypotheses type the premises at $S_{2} ε_{1}$ and $ε_{2}$ ; unifier soundness proves $S_{2} ε_{1} \equiv ε_{2}$ , and C-To gives W’s substituted result.

For let, the accumulator invariant transports the bound judgment before unification establishes the empty effect required by C-Let. Then lemma 25.16 justifies the environment scheme, and the induction hypothesis types the body. For a handler, the invariant transports the body, return, and each operation-clause judgment in the fixed clause order. The sequential unifications establish exactly (25.14), a return clause of result $β! μ$ , and operation clauses of that result under $p_{i} : P_{i}$ and $k_{i} : R_{i} \overset{μ}{\to} β$ . These are the premises of C-Handle. ◻

Lemma 31.21 — Non-handler factorization step ¶

Consider a declarative value or computation derivation whose last rule is not C-Handle. Suppose that the principal-factorization conclusion holds for each immediate typing premise of that last rule. Then W succeeds on the conclusion. For a computation conclusion $T Γ ⊢ e : A! ε$ , if $W_{c} (Γ, e) = (S, A_{0}, ε_{0})$ , there is a substitution $Q$ such that $\begin{matrix} (31.15) & T Γ \equiv Q S Γ, A \equiv Q A_{0}, ε \equiv Q ε_{0} . \end{matrix}$ For a value conclusion $T Γ ⊢_{v} v : A$ , $W_{v} (Γ, v) = (S, A_{0})$ succeeds, and there is a substitution $Q$ such that $T Γ \equiv Q S Γ, A \equiv Q A_{0} .$

Referenced from 3 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Lemma 31.21 — Non-handler factorization step

Proof. Inspect the last rule, using the assumed factorization for each immediate typing premise.

Ordinary forms. The value and computation cases use the common factorization statement (25.15). A declarative variable instance factors through W’s fresh instance by mapping each fresh variable to the type chosen in the derivation. A declarative constant instance factors in the same way through W’s fresh instance of its closed declaration. In the lambda case, inversion gives a monomorphic parameter type and the corresponding body derivation. Map W’s fresh parameter variable to that type and apply the assumed computation factorization to the body. In the return case, apply the assumed value factorization and map W’s fresh $μ$ to the derivation’s chosen effect row.

Application, operation, and sequencing. For application, inversion yields types $A$ and $B$ such that the operator has type $A \overset{ε}{\to} B$ and the argument has type $A$ . The two value hypotheses first factor their inferences; the residual declarative substitution then unifies W’s generated arrow equation. MGU factorization produces the next residual $Q$ . For an operation, the assumed value factorization handles the parameter inference; the residual declarative substitution then unifies W’s equation with $P_{ℓ}$ , after which the declarative tail is the image of W’s fresh $μ$ . For sequencing, the two computation hypotheses factor the subterms from left to right; inversion says their effects are equivalent, so the residual substitution solves W’s effect equation. The row MGU theorem factors it once more. These compositions give all three equations in (25.15).

Pure let. In the let case, inversion gives an empty effect. The assumed factorization followed by MGU factorization reaches W’s empty-row unifier. Lemma 25.16 factors the scheme used by the declarative body through W’s generalized scheme. Apply the assumed body factorization and compose.

Row conversion. If the last rule is C-RowConv, write its premise effect as $ε^{-}$ , so $ε^{-} \equiv ε$ . The assumed premise factorization premise factors the same syntax-directed W run as $W_{c} (Γ, e) = (S, A_{0}, ε_{0})$ , with residual $Q$ such that $T Γ \equiv Q S Γ$ , $A \equiv Q A_{0}$ , and $ε^{-} \equiv Q ε_{0}$ . Symmetry and transitivity give $ε \equiv Q ε_{0}$ , so the same $Q$ proves (25.15) for the converted conclusion; W needs no additional equation or solve step. ◻

Lemma 31.22 — Handler-accumulator factorization step ¶

Suppose the last rule is C-Handle, and suppose the principal-factorization conclusion holds for its body, return clause, and operation clauses. Then the handler run of $W_{c}$ succeeds and produces $(S, A_{0}, ε_{0})$ with a residual $Q$ satisfying (25.15).

Referenced from 3 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Lemma 31.22 — Handler-accumulator factorization step

Proof. For a handler, invert C-Handle and follow the accumulator literally. Before following its premises, extend the declarative substitution $T$ to each fresh W variable by the type or row selected by the inverted declarative derivation. The fresh variables lie outside the original domain, so the two parts of the extension are disjoint. After accumulator stage $j$ , maintain a residual substitution $Θ_{j}$ with $\begin{matrix} (31.16) & \begin{aligned} T & = Θ_{j} Q_{j} & on the environment variables and every fresh variable \\ introduced through stage j . \end{aligned} \end{matrix}$ The assumed body factorization initializes this invariant at $Q_{0} = S_{0}$ . For the return clause, its assumed factorization handles the declarative clause derivation through $S_{r} Q_{0}$ . Inversion says that the declarative return type and effect are the handler’s $β$ and $μ$ . The residual sends the fresh reported type variable to the inverted declarative result and therefore unifies the first oriented equation $Q_{r}^{0} B_{r} ≐ Q_{r}^{0} β$ . After that MGU is composed, the residual sends the fresh row variable to the inverted declarative effect and unifies the second equation $Q_{r}^{1} δ_{r} ≐ Q_{r}^{1} μ$ . The MGU factorization theorem factors it through $Q_{r}^{1}$ and then $Q_{r}$ , establishing (25.16) after the return stage.

Suppose (25.16) holds before clause $i$ . Its assumed factorization handles the declarative clause derivation through $S_{i} Q_{i - 1}^{c}$ . The inverted clause premise gives the expected type $T β$ , effect $T μ$ , and continuation type $T R_{i} \overset{T μ}{\to} T β$ . Thus the residual solves the reported-type equation and then the reported-effect equation. Two MGU factorizations yield $Q_{i}^{1}$ and $Q_{i}^{c}$ , preserving the invariant. Induction over the fixed clause order reaches $Q_{n}^{c}$ . Finally, the inverted handler-input premise solves the row equation in (25.14); one last MGU factorization yields $Q^{'}$ and its residual. This is the required factor $Q$ in (25.15). ◻

Theorem 25.18 — Completeness and principal factorization ¶

Suppose $T Γ ⊢ e : A! ε$ . Then $W_{c} (Γ, e) = (S, A_{0}, ε_{0})$ succeeds, and there is a substitution $Q$ satisfying (25.15). If $T Γ ⊢_{v} v : A$ , then $W_{v} (Γ, v) = (S, A_{0})$ succeeds, and there is a substitution $Q$ such that $T Γ \equiv Q S Γ, A \equiv Q A_{0} .$ Thus, for an empty environment, ${gen}_{c} (\emptyset, A_{0}! ε_{0})$ is the principal computation scheme.

Referenced from 5 locations

Proof of Theorem 25.18 — Completeness and principal factorization

Proof. Proceed by simultaneous induction on value and computation derivations. At every last rule other than C-Handle, apply lemma 31.21 to the induction hypotheses for its immediate typing premises. At C-Handle, apply lemma 31.22 to the body, return, and clause induction hypotheses. These cases exhaust the declarative rules and establish both factorization statements. For $Γ = \emptyset$ , lemma 25.16 turns the computation factorization into the displayed principal scheme. ◻

Here is the complete row part of W on the transaction. Name the fresh tail of the final return $ρ_{r}$ , the tail of $put$ by $ρ_{p}$ , the instantiated callback tail by $ρ_{f}$ , and the tail of $get$ by $ρ_{g}$ . Working from the final sequence outward, W generates the following equations and MGUs: $\begin{array}{cc} equation & new bindings \\ ⟨ put ∣ ρ_{p} ⟩ ≐ ρ_{r} & ρ_{r} \mapsto ⟨ put ∣ ρ_{p} ⟩ \\ ⟨ raise ∣ ρ_{f} ⟩ ≐ ⟨ put ∣ ρ_{p} ⟩ & ρ_{p} \mapsto ⟨ raise ∣ ξ ⟩, ρ_{f} \mapsto ⟨ put ∣ ξ ⟩ \\ ⟨ get ∣ ρ_{g} ⟩ ≐ ⟨ put, raise ∣ ξ ⟩ & ξ \mapsto ⟨ get ∣ μ ⟩, ρ_{g} \mapsto ⟨ put, raise ∣ μ ⟩ . \end{array}$ For the second equation, exposure skips $put$ , expands $ρ_{p}$ with $raise$ , and leaves residual $⟨ put ∣ ξ ⟩$ . For the third it skips $put, raise$ , expands $ξ$ with $get$ , and leaves residual $⟨ put, raise ∣ μ ⟩$ . Thus the composite substitution is $\begin{aligned} ρ_{r} & \mapsto ⟨ put, raise, get ∣ μ ⟩, & ρ_{p} & \mapsto ⟨ raise, get ∣ μ ⟩, \\ ρ_{f} & \mapsto ⟨ put, get ∣ μ ⟩, & ξ & \mapsto ⟨ get ∣ μ ⟩, \\ ρ_{g} & \mapsto ⟨ put, raise ∣ μ ⟩ . \end{aligned}$ The callback instance is therefore $ν = ρ_{f} = ⟨ get, put ∣ μ ⟩$ , modulo exchange, and every sequencing node has common effect $E_{μ}$ . Since $μ \notin ftv (Γ_{f})$ , computation generalization gives ${gen}_{c} (Γ_{f}, Int! E_{μ}) = \forall μ . (Int! E_{μ})$ , as in (25.2). For the monomorphic value $λ f . t_{f}$ , W instead gives $f : 1 \overset{ε_{f}}{\to} Int$ a fresh monotype. Its row equations are $\begin{array}{cc} equation & new bindings \\ ⟨ put ∣ ρ_{p} ⟩ ≐ ρ_{r} & ρ_{r} \mapsto ⟨ put ∣ ρ_{p} ⟩ \\ ε_{f} ≐ ⟨ put ∣ ρ_{p} ⟩ & ε_{f} \mapsto ⟨ put ∣ ρ_{p} ⟩ \\ ⟨ get ∣ ρ_{g} ⟩ ≐ ⟨ put ∣ ρ_{p} ⟩ & ρ_{p} \mapsto ⟨ get ∣ μ ⟩, ρ_{g} \mapsto ⟨ put ∣ μ ⟩ . \end{array}$ Thus the common row is $G_{μ}$ , and V-Lam gives (25.3). This is the promised full trace; no handler-specific heuristic occurs in it.

We can now compare four handlers at one formal signature. Write $Γ ⊢ H : A! ε_{in} ⟹ B! ε_{out}$ as an abbreviation for the return- and operation-clause premises of C-Handle, with those input and output rows. Combining those premises with $Γ ⊢ e : A! ε_{in}$ in C-Handle gives $Γ ⊢ handle e with H : B! ε_{out}$ .

The fallback handler already calculated above satisfies $d : B ⊢ C_{d}^{B} : B! ⟨ raise ∣ μ ⟩ ⟹ B! μ .$ For a reader environment $r : Env$ , define $H_{ask}^{r} = {return x \mapsto return x; ask (u; k) \mapsto k r} .$ The two premises are $x : A ⊢ return x : A! μ, u : 1, k : Env \overset{μ}{\to} A ⊢ k r : A! μ,$ so $r : Env ⊢ H_{ask}^{r} : A! ⟨ ask ∣ μ ⟩ ⟹ A! μ$ .

Here is the one-clause handler accumulator once in full. For $h_{r} = handle (perform ask ()) with H_{ask}^{r}$ , the body reports $Env! ⟨ ask ∣ μ_{0} ⟩$ . Choose output variables $β, μ$ . The return clause reports $Env! δ_{r}$ , so its two solve steps bind $β \mapsto Env$ and $δ_{r} \mapsto μ$ . The operation context is then constructed as $u : 1, k : Env \overset{μ}{\to} Env, r : Env .$ Its body $k r$ already reports $Env! μ$ , so the clause’s two solve steps are identities. The final input equation $⟨ ask ∣ μ_{0} ⟩ ≐ ⟨ ask ∣ μ ⟩$ binds $μ_{0} \mapsto μ$ . Thus W returns $Env! μ$ , with relative scheme $\forall μ . (Env! μ)$ . The continuation’s output row is chosen when its context entry is constructed; it is not discovered by a later equation.

For a second comparison, add the operation $Σ (choose) = 1 ⇝ Bool .$ The next handler deliberately resumes twice: $\begin{aligned} H_{twice} = { & return x \mapsto return x; \\ choose (u; k) \mapsto k true to x . k false} . \end{aligned}$ Here $x : 1$ is intentionally unused. Both applications of $k : Bool \overset{μ}{\to} 1$ have result $1! μ$ ; C-To therefore derives the clause, while the return clause is $x : 1 ⊢ return x : 1! μ$ . Hence $⊢ H_{twice} : 1! ⟨ choose ∣ μ ⟩ ⟹ 1! μ .$ Although $k$ occurs twice, C-To derives the clause because it places no affine-use premise on the continuation variable.

Finally define a state-passing handler for unit-returning computations: $\begin{aligned} H_{st} = { & return x \mapsto return (λ s . return s); \\ get (u; k) \mapsto return (λ s . k s to g . g s); \\ put (s^{'}; k) \mapsto return (λ s . k () to g . g s^{'})} . \end{aligned}$ Put $D = Int \overset{μ}{\to} Int$ . The return clause has type $D! μ$ . In the get clause, $k : Int \overset{μ}{\to} D$ ; both $k s$ and $g s$ have effect $μ$ , so the lambda has type $D$ . In the put clause, $k : 1 \overset{μ}{\to} D$ ; the same derivation ends in $g s^{'}$ . Thus $⊢ H_{st} : 1! ⟨ get, put ∣ μ ⟩ ⟹ D! μ .$ The exception, reader, choice, and state examples all use the same final row equation in W. Only their clause terms differ.

Exercise 25.7 — W on the transaction ¶

★★★ Insert $perform \log e to w$ after the put in $t_{f}$ , with $e : Error$ , and run W on the monomorphic wrapper. Name the fresh row variables and show that the callback and body share the principal row $⟨ get, put, \log ∣ μ ⟩$ . Then instantiate its tail with one $raise$ and compare that instance with the separate let-polymorphic callback trace above.

Referenced from 3 locations

Exercise 25.8 — W on a deep handler ¶

★★☆ In the context $r : Env$ , run W on the fully specified computation $h_{r} = handle (perform ask ()) with H_{ask}^{r} .$ Name the fresh variables and the accumulator substitutions after the body, return clause, operation clause, and input-row equation; then give the principal computation scheme relative to $r : Env$ . Point to the accumulator extension where the continuation is constructed with the output row $μ$ , and explain why using the handler’s input row there would be unsound.

Referenced from 3 locations

The duplicate-free bridge to set-indexed effects

Row polymorphism here is ordinary kinded quantification. A scheme may quantify $μ$ , and duplicate labels make extension and elimination unconstrained. There are no type classes, qualified types, subeffect inequalities, or predicates $ℓ \notin μ$ . Adding any of those changes both principal schemes and the solver theorem. The MGU theorem is not a theorem about unique-label rows with hidden lacks constraints.

The set-indexed calculus forgets multiplicity. For any closed row, write $⌊ ε ⌋$ for its finite support: the set of labels occurring at least once. The target signature is $⌊ Σ ⌋ (ℓ) = ⌊ P_{ℓ} ⌋ ⇝ ⌊ R_{ℓ} ⌋$ . Translate by $\begin{matrix} (31.17) & \begin{array}{rcl} ⌊ A \overset{ε}{\to} B ⌋ & = & U_{\emptyset} (⌊ A ⌋ \Rightarrow^{⌊ ε ⌋} F ⌊ B ⌋), \\ ⌊ λ x . e ⌋ & = & thunk (λ x . ⌊ e ⌋), \\ ⌊ v w ⌋ & = & (force ⌊ v ⌋) ⌊ w ⌋, \\ ⌊ return v ⌋ & = & return ⌊ v ⌋, \\ ⌊ e_{1} to x . e_{2} ⌋ & = & ⌊ e_{1} ⌋ to x . ⌊ e_{2} ⌋, \\ ⌊ perform ℓ v ⌋ & = & ℓ ⌊ v ⌋ (x . return x), \\ ⌊ handle e with H ⌋ & = & handle ⌊ e ⌋ with ⌊ H ⌋ . \end{array} \end{matrix}$ Variables and base constants map to themselves, and handlers map clause by clause: $⌊ H ⌋ = {return x \mapsto ⌊ e_{r} ⌋; ℓ_{i} (p_{i}; k_{i}) \mapsto ⌊ e_{i} ⌋}_{i = 1}^{n} .$ Contexts map pointwise: $⌊ Γ, x : A ⌋ = ⌊ Γ ⌋, x : ⌊ A ⌋$ . Within a translated clause, a source call $k_{i} v$ is $(force k_{i}) ⌊ v ⌋$ , because the CBPV handler binds its continuation as a thunk. A computation type $A! ε$ maps to $F ⌊ A ⌋! ⌊ ε ⌋$ .

The target handler rule of chapter 22 checks each continuation at the chosen output set $E_{out}$ , requires $E_{in} ∖ H \subseteq E_{out}$ , and admits ordinary effect weakening. The translation proof establishes precisely these continuation, residual- inclusion, and weakening premises; it does not require equality of the two effect sets.

Theorem 25.19 — Closed-row support translation ¶

Call a derivation monomorphic when every variable assumption has a scheme with no quantified type or row variables. Require every constant instantiation to be fixed before the derivation begins. If such a derivation contains no C-Let root and uses only closed rows, then the judgment $Γ ⊢ e : A! ε$ yields $\begin{aligned} ⌊ Γ ⌋ & ⊢_{c} ⌊ e ⌋ : \\ F ⌊ A ⌋! ⌊ ε ⌋ \end{aligned}$ in the set-indexed CBPV core. A source value judgment $Γ ⊢_{v} v : A$ yields the value judgment $⌊ Γ ⌋ ⊢_{v} ⌊ v ⌋ : ⌊ A ⌋$ .

Referenced from 3 locations

Proof of Theorem 25.19 — Closed-row support translation

Proof. Induct on typing. A source return first uses the pure CBPV return rule and then effect weakening; an atomic operation uses an explicit pure return continuation and then weakening to the translated tail. Sequencing uses $E \cup E = E$ . Lambda, force/application, and the remaining value rules are the corresponding CBPV rules after type translation. The let-free hypothesis removes the only rule whose target would require polymorphic schemes, which the chapter 22 core does not contain. A C-RowConv step translates to the identical target annotation because row exchange does not change the underlying finite set.

It remains to check the displayed handler clause. Invert C-Handle and write $H = {ℓ_{1}, \dots, ℓ_{n}}, E = ⌊ ε ⌋, E_{in} = H \cup E .$ The body induction hypothesis gives $⌊ Γ ⌋ ⊢_{c} ⌊ e ⌋ : F ⌊ A ⌋! E_{in}$ , and the return-clause hypothesis gives $⌊ e_{r} ⌋ : F ⌊ B ⌋! E$ under $x : ⌊ A ⌋$ . For operation clause $i$ , type translation maps the source resumption assumption $k_{i} : R_{i} \overset{ε}{\to} B$ exactly to $p_{i} : ⌊ P_{i} ⌋, k_{i} : U_{\emptyset} (⌊ R_{i} ⌋ \Rightarrow^{E} F ⌊ B ⌋) .$ The clause induction hypothesis therefore types $⌊ e_{i} ⌋$ at $F ⌊ B ⌋! E$ under the target parameter and resumption binders; its calls use $(force k_{i}) ⌊ v ⌋$ , as specified above. For arbitrary multiplicities, set algebra gives $E_{in} ∖ H = (H \cup E) ∖ H \subseteq E .$ This inclusion discharges the residual-effect premise of target C-Handle; the return and operation-clause induction hypotheses discharge its remaining premises. Hence the translated handler has type $F ⌊ B ⌋! E$ . ◻

For a concrete covered term, fix $e_{0} : Error$ . The closed, duplicate-free judgment $\cdot ⊢ perform \log e_{0} : 1! ⟨ \log ⟩$ translates to $\log e_{0} (x . return x)$ , typed in the set core at $F 1! {\log}$ . A closed-row fallback handler gives the corresponding one-clause handler example.

The target calculus makes an operation’s continuation part of the operation node, whereas the row calculus first exposes an atomic request and lets an evaluation context supply its continuation. Its target also has administrative force/thunk steps and algebraic reassociation of sequencing. A simulation theorem would therefore need an explicit target closure modulo those equations and a proof that every source context maps to that closure. The theorem is a typing bridge rather than a simulation. Its information loss is visible on the rethrower: the target handler premise is an inclusion, so erasing both input and output to a set containing $raise$ still typechecks. What erasure cannot express is which occurrence was discharged. On duplicate-free closed rows, support is injective up to row exchange; on rows with multiplicity, distinct source annotations collapse. Consequently support erasure is not faithful on general rows.

Generalized evidence passing

The inference calculus above and the following compilation calculus share scoped rows, but they have different endpoints. Freeze Xie and Leijen’s explicitly typed System $F_{ε}$ source with $σ ::= α^{κ} ∣ c^{κ} \bar{σ} ∣ σ_{1} \to^{ε} σ_{2} ∣ \forall α^{κ} . σ, ε ::= ⟨ ⟩ ∣ ⟨ ℓ ∣ ε ⟩ ∣ α^{eff} .$ The prompt/evidence intermediate $F_{p w}$ adds internal terms $prompt m h e$ and $yield m v$ . Evidence and evidence vectors have the exact forms $q ::= (m, h, w), w ::= ⟨ ⟩ ⟩ ∣ ⟨ ℓ : q ∣ w ⟩ ⟩ .$ Selection must find the most recently extended evidence: $⟨ ℓ : q ∣ w ⟩ ⟩ . ℓ = q, ⟨ ℓ^{'} : q ∣ w ⟩ ⟩ . ℓ = w . ℓ (ℓ \neq ℓ^{'}) .$ The third component stores the evidence context in which $h$ was defined. The $F_{p w}$ fragment frozen here retains that source representation but does not inspect the selected tail $w^{'}$ in its displayed perform step. The source’s later tail-resumptive optimization gives the component operational work through an $under$ frame; that optimization and its rules are outside this card.

On a performed operation, evidence selection replaces dynamic search: $\begin{array}{r} w ⊢ perform op ε_{0} \bar{σ} v ⇝_{0} yield m (λ^{ε} k . f \bar{σ} v k) \end{array}$ when $w . ℓ = (m, h, w^{'})$ , the clause $(op \mapsto f)$ occurs in $h$ , and the global signature assigns $op$ to $ℓ$ . A prompt extends the current evidence vector by $⟨ ℓ : (m, h, w) ∣ w ⟩ ⟩$ while evaluating its body. Thus the selected evidence and the nearest dynamic prompt agree only under a reachability invariant.

Definition 31.25 — Internal safety ¶

An $F_{p w}$ expression $e$ is internal-safe when there is a closed, well-typed expression $e_{0}$ , containing no $prompt$ , $yield$ , or marker, such that $⟨ ⟩ ⟩ ⊢ e_{0} ⟶^{*} e .$

Referenced from 4 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

This is Definition 1 of the source read as its least fixed point, rather than as a circular closure clause. It ensures that each prompt owns a unique marker generated by the handler rule and that every yielded marker came from type-correct evidence selection. Arbitrary user-written prompt or yield terms are outside the definition.

Theorem 31.26 — Internal-safe preservation ¶

If $\cdot ⊢ e : σ ∣ ⟨ ⟩$ , $e$ is internal-safe, and $⟨ ⟩ ⟩ ⊢ e ⟶ e^{'}$ , then $\cdot ⊢ e^{'} : σ ∣ ⟨ ⟩$ .

Referenced from 2 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Theorem 31.26 — Internal-safe preservation

Source import. This is Theorem 2, §3.1.4, pp. 18–19 of [XL21]. Its induction uses the clause-typing and generated-marker invariants of definition 31.25. ◻

Theorem 31.27 — Internal-safe progress ¶

If $\cdot ⊢ e : σ ∣ ⟨ ⟩$ and $e$ is internal-safe, then $e$ is a value or there are $w, e^{'}$ with $w ⊢ e ⟶ e^{'}$ .

Referenced from 2 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Theorem 31.27 — Internal-safe progress

Source import. This is Theorem 3 at the same source location. Source Theorem 1, immediately before Definition 1 on p. 19, relates evidence-indexed reduction to the evidence extracted from the evaluation context and supplies the selected handler in the request case. ◻

Theorem 31.28 — Live-marker uniqueness ¶

If an internal-safe expression contains $prompt m_{1} h_{1} (E_{2} [prompt m_{2} h_{2} e]),$ then $m_{1} \neq m_{2}$ .

Referenced from 3 locations

Proof of Theorem 31.28 — Live-marker uniqueness

Source import. This is Theorem 4, §3.1.4, p. 19 of [XL21]. Both markers arise from reachable handler-generated prompts; the theorem’s distinct-marker invariant therefore applies to the displayed nesting. ◻

The next intermediate $F_{p b}$ propagates a $yield m f k$ term outward through evaluation contexts, so the monadic translation can realize it as the $Yield$ constructor of the target control monad. The target is a plain higher-kinded polymorphic lambda calculus with $Mon ε A : = Evv ε \to Ctl ε A,$ where a translated computation accepts its evidence vector explicitly. Translation is type directed: $Γ ⊢ e : σ ∣ ε ⇝ e^{'} .$ Values become functions returning $Pure$ ; application sequences the two translated computations by monadic bind, $⟨ ⟨ e_{1} e_{2} ⟩ ⟩_{gep} = ⟨ ⟨ e_{1} ⟩ ⟩_{gep} ▹ (λ f . ⟨ ⟨ e_{2} ⟩ ⟩_{gep} ▹ f);$ a performed operation uses the evidence selector for its label, for example $\begin{aligned} ⟨ ⟨ v ⟩ ⟩_{gep} & = λ w : Evv ε . Pure ε ⟨ ⟨ σ ⟩ ⟩_{gep} ⟨ ⟨ v ⟩ ⟩_{gep, v}, \\ ⟨ ⟨ perform op ⟩ ⟩_{gep} & = {perform}_{ℓ} (select op) . \end{aligned}$ The complete target and representative translation rules are frozen in subappendix A.28.

Theorem 31.29 — Generalized-evidence operational endpoint ¶

Let $e$ be a closed System- $F_{ε}$ program and let $\cdot ⊢ e : Int ∣ ⟨ ⟩ ⇝ e^{'} .$ If $e ⟶^{*} n$ , then $e^{'} ⟨ ⟩ ⟩ ⟶^{*} Pure ⟨ ⟩ Int n .$ If $e$ diverges, then $e^{'} ⟨ ⟩ ⟩$ diverges.

Referenced from 2 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Theorem 31.29 — Generalized-evidence operational endpoint

Source import. This is Theorem 7, §4.4, p. 25 of the version-4 report [XL21]. Its proof composes the source to multi-prompt simulation (Theorem 14), evidence-passing simulation (Theorem 15), bubbling simulation (Theorem 18), and monadic simulation (Theorem 19). The statement requires a closed integer source, empty source row, empty initial evidence vector, and the final $Pure$ result. It states neither arbitrary-open-program correctness nor correctness of generated C. ◻

The pinned MpEff release implements insertion-ordered generalized evidence vectors as a Haskell library. It does not contain the mechanized proofs and is not the Koka-to-C compiler. Current Koka uses canonical evidence and further optimizations. Results from either implementation are artifact evidence, not new hypotheses for theorem 25.18.

Exercise 31.9 — Selection and marker provenance ¶

★★☆ Build two nested evidence entries for the same label $ℓ$ , with distinct markers $m_{o}$ and $m_{i}$ . Calculate selection of the newest entry and the resulting $yield$ term. Then explain which definition 31.25 invariant rules out reusing $m_{o}$ for the inner prompt. State separately why the displayed $F_{p w}$ perform step does not inspect the selected entry’s third component.

Referenced from 3 locations

Effect exclusion is a separate calculus

An open duplicate row $⟨ ℓ ∣ μ ⟩$ states that $ℓ$ is present. It cannot state that $ℓ$ is absent from the unknown tail $μ$ . For example, a recovery combinator may require its handler argument to perform any effects except $raise$ . Neither $μ$ nor $⟨ raise ∣ μ ⟩$ expresses that negative premise.

The calculus $λ_{∁}$ solves a different problem. Fix a finite closed universe $U$ of effects and take Boolean formulas $φ ::= β ∣ \emptyset ∣ {F} ∣ φ^{c} ∣ φ \cup φ ∣ φ \cap φ, φ ∖ ψ : = φ \cap ψ^{c} .$ Formulas are identified by equality under every valuation, $φ \equiv_{B} ψ$ . Function types carry latent formulas. There is no subeffecting rule.

The term $e without F$ pushes a stack frame forbidding $F$ . To keep the source’s $T$ -prefixed rules distinct from the adjacent System- $Xi$ card, this book uses the prefix $Ex$ . Its typing rule is $\frac{Γ ⊢_{∁} e : τ ∣ φ φ \cap {F} \equiv_{B} \emptyset}{Γ ⊢_{∁} e without F : τ ∣ φ} Ex - Without .$ At runtime, $do F (v)$ steps only when $F \notin forb (k)$ . The local machine interface is $\begin{aligned} W_{F} & : = [] without F, & L_{x, e} & : = let x = [] in e, \\ k & ::= ∙ ∣ W_{F} :: k ∣ L_{x, e} :: k, \\ forb (∙) & = \emptyset, \\ forb (W_{F} :: k) & = {F} \cup forb (k), \\ forb (L_{x, e} :: k) & = forb (k) . \end{aligned}$ A configuration is $⟨ e ∣ k ⟩$ . The machine judgment is $⊢_{m} ⟨ e ∣ k ⟩ ok$ ; the stack judgment $τ ⊢_{k} k ∖ φ$ records the formula forbidden by $k$ . Here $∖$ is the source’s judgment separator, not the Boolean difference operation in $φ ∖ ψ$ . The exact machine and stack rules in subappendix A.28 maintain disjointness between performed and forbidden effects.

Theorem 31.30 — Effect exclusion safety ¶

If $⊢_{m} ⟨ do F (v) ∣ k ⟩ ok$ , then $F \notin forb (k) .$

Referenced from 3 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Theorem 31.30 — Effect exclusion safety

Source import. This is Theorem 3.14, §3.4, p. 16 of Lutze et al. [LMSB23]. Inversion of machine typing gives a performed formula $φ_{1}$ , a forbidden formula $φ_{2}$ , and $φ_{1} \cap φ_{2} \equiv_{B} \emptyset$ . Lemma 3.12 identifies $φ_{1}$ with ${F}$ ; Lemma 3.13 identifies $φ_{2}$ with $forb (k)$ . ◻

Theorem 31.31 — Effect-exclusion machine safety ¶

A well-typed machine is final or takes a step, and machine typing is preserved by every step.

Referenced from 2 locations

Effect Rows, Principal Type-and-Effect Inference, and Handlers

Proof of Theorem 31.31 — Effect-exclusion machine safety

Source import. Progress and preservation are Theorems 3.10–3.11, §3.4, p. 15 of [LMSB23]. The progress proof uses theorem 31.30 in its T-Do case. Preservation is a separate case analysis on the machine step and does not depend on effect exclusion safety. ◻

This theorem belongs to the fixed-universe Boolean row theory. Its principal types are principal only modulo Boolean equivalence, and its inference uses Boolean unification. None of these facts follows from the duplicate-label MGU of theorem 25.14; conversely, the exclusion paper and its VM artifact prove no theorem about the inference calculus of this chapter.

Exercise 31.10 — A negative row witness ¶

★★☆ Give a type for a recovery combinator whose handler may perform effects $β ∖ {raise}$ . Derive its Ex-Without premise, then show why neither an open row variable $μ$ nor one positive extension of $μ$ entails the required absence statement.

Referenced from 3 locations

The row choice and exposure unifier follow Leijen’s scoped-label development [Lei05]. Koka uses duplicate labels and a closely related inference algorithm [Lei14]. It uses duplicate effect labels for the same reason and proves soundness and principality for its own syntax-directed system; the deep-handler calculus and set-erasure theorem above are proved locally.

Exercise 25.9 — The multiplicity boundary ¶

★★☆ Apply set erasure to the pure and rethrowing catches. Show which two distinct rows $⟨ raise, raise ∣ ν ⟩$ and $⟨ raise ∣ ν ⟩$ collapse to one set. Show that the rethrower’s erased target handler nevertheless satisfies the target premise $E_{in} ∖ H \subseteq E_{out}$ . Compare this with a fallback whose output contains no $raise$ , and explain exactly which multiplicity information is lost even though typing is preserved.

Referenced from 3 locations

Exercise 25.10 — Qualified alternative ¶

★★☆ Redesign row extension so labels are unique. State the lacks constraint needed to extend $μ$ by $ℓ$ . Rewrite the one-clause instance of C-Handle and W’s final input-row equation with that premise. List the soundness, completeness, constraint-entailment, and factorization properties needed before a principality theorem could be claimed.

Referenced from 3 locations

Suggested first pass.

Begin with exercise 25.11, continue with exercise 25.12, and finish with exercise 25.13.

Exercise 25.11 ¶

★★☆ Prove the factorization half of lemma 25.12 when the visible prefix has two equal skipped labels. Display the exchanges, cancellation, and residual factor; identify the step that needs multiplicity.

Referenced from 4 locations

Exercise 25.12 ¶

★★★ Give the complete one-operation handler case of Theorem 25.18. Give the residual after the body, return clause, operation clause, and input-row equation, then pair every equation with its rule, MGU, and factor.

Referenced from 4 locations

Exercise 25.13 ¶

★★☆ Nest a handler that forwards $raise$ inside one that handles it. Derive the types of both reduction roots, then use multiplicities and Theorem 25.10 to exclude an exposed request when the final effect is empty.

Referenced from 4 locations

Exercise 25.14 — (*)¶

★★★ Replace duplicate labels by unique rows plus lacks constraints. State a well-kinded exposure judgment with its lacks premise, its factorization theorem, and the one-operation handler case of W. Compare these proof obligations with those of (25.11).

Referenced from 3 locations

Exercise 25.15 ¶

★★★ Practical project.effect-row-inferencer Implement the finite row and handler fragment in Kappa. Represent open rows with duplicate-preserving prefixes; implement exchange comparison, single-occurrence cancellation, guarded exposure, and the one-layer handler transition. The permanent corpus must distinguish exchange from contraction, remove exactly one duplicate, compute one open-row MGU, reject the shared-tail cycle by the guard rather than fuel exhaustion, retain $get$ , $put$ , and $raise$ in the transaction trace, forward once to the nearest handler, leave one $raise$ for an outer fallback, and construct the reader resumption with the handler output tail. The oracle is the ordered list of these eight results. As a semantic mutation, recurse on the unmodified right row in prefix comparison; it must still type-check and audit cleanly but fail the oracle. Appendix E records the four acceptance commands, and appendix F gives the implementation stages.

Referenced from 4 locations