ch:effect-rows: ch:effect-rows

Fix the tail symbol and interpret a row prefix as its finite multiplicity function $m:\mathsf{Label}\to \mathbb{N}$. Then $$m_{⟨\ell ,\ell \mid \mu ⟩}(\ell )=2+m_{\mu }(\ell ),m_{⟨\ell \mid \mu ⟩}(\ell )=1+m_{\mu }(\ell ).$$ Natural-number cancellation would equate $2$ and $1$, so the rows are not equivalent. Operationally, a handler can consume the first occurrence and re-perform $\ell$ in its clause. Its input and output effects are therefore $⟨\ell ,\ell \mid \mu ⟩$ and $⟨\ell \mid \mu ⟩$. Contraction would identify those types and erase the fact that the outer request remains observable.

Put $\nu =⟨\mathsf{get},\mathsf{put}\mid \xi ⟩$. The fallback instance has premises $$\begin{array}{c}\mathrm{\Gamma }⊢e:\mathsf{Int}!⟨\mathsf{raise}\mid \nu ⟩,\\ \mathrm{\Gamma },x:\mathsf{Int}⊢\mathsf{return}x:\mathsf{Int}!\nu ,\\ \mathrm{\Gamma },p:\mathsf{Error},k:\mathbf{0}\stackrel{\nu }{\to }\mathsf{Int}⊢\mathsf{return}d:\mathsf{Int}!\nu .\end{array}$$ Thus C-Handle changes $\mathsf{Int}!⟨\mathsf{raise},\mathsf{get},\mathsf{put}\mid \xi ⟩$ to $\mathsf{Int}!⟨\mathsf{get},\mathsf{put}\mid \xi ⟩$.

For the rethrower put $\epsilon =⟨\mathsf{raise},\mathsf{get},\mathsf{put}\mid \xi ⟩$. Its premises are $$\begin{array}{c}\mathrm{\Gamma }⊢e:\mathsf{Int}!⟨\mathsf{raise}\mid \epsilon ⟩,\\ \mathrm{\Gamma },x:\mathsf{Int}⊢\mathsf{return}x:\mathsf{Int}!\epsilon ,\\ \mathrm{\Gamma },p:\mathsf{Error},k:\mathbf{0}\stackrel{\epsilon }{\to }\mathsf{Int}⊢\mathsf{perform}\mathsf{raise}p\mathsf{to}z.kz:\mathsf{Int}!\epsilon .\end{array}$$ The last premise follows from C-Op at result $\mathbf{0}$ and C-To; no value of $\mathbf{0}$ is required. This instance changes $\mathsf{Int}!⟨\mathsf{raise},\mathsf{raise},\mathsf{get},\mathsf{put}\mid \xi ⟩$ to $\mathsf{Int}!\epsilon$.

Write the initial computation as $M_0$. Its innermost handler is $H_0$, so H-Forward gives For $M_0$, lemma 25.6 has outside context $E^{\prime }=\mathsf{handle}[]\mathsf{with}{H}_1$, request context $R$, and nearest handler $H_0$. In $M_1$ the request context immediately inside $H_1$ is $$R_1=[]\mathsf{to}y.\mathsf{handle}R[\mathsf{return}y]\mathsf{with}{H}_0.$$ Hence H-Op gives $$M_1⟶e_{\ell }[v/p,(\lambda z.\mathsf{handle}{R}_1[\mathsf{return}z]\mathsf{with}{H}_1)/k].$$ The first body is syntactically $\mathsf{handle}R[\mathsf{perform}\ell v]\mathsf{with}{H}_0$; because it contains a handler frame, it cannot be $R^{\prime }[\mathsf{perform}\ell v]$ for handler-free $R^{\prime }$. Thus the outer H-Op is not an initial root.

Invert the typing of $\mathsf{handle}R[\mathsf{perform}\ell v]\mathsf{with}H$. If $H$ handles ${\ell }_1,\dots ,{\ell }_n$ and has output row $\epsilon$, the handler premise and typed hole give $$⟨{\ell }_1,\dots ,{\ell }_n\mid \epsilon ⟩\equiv ⟨\ell \mid \delta ⟩,\ell \notin \{{\ell }_1,\dots ,{\ell }_n\}.$$ The second part of cancellation exposes $\epsilon \equiv ⟨\ell \mid {\epsilon }^{\prime }⟩$. For fresh $y:R_{\ell }$, C-Return types the replacement hole $\mathsf{return}y:R_{\ell }!\delta$. Request-context replacement therefore reconstructs the input premise, and C-Handle gives $$\mathrm{\Gamma },y:R_{\ell }⊢\mathsf{handle}R[\mathsf{return}y]\mathsf{with}H:B!\epsilon .$$ Choose ${\epsilon }^{\prime }$ as the tail in C-Op; the forwarded request then has effect $⟨\ell \mid {\epsilon }^{\prime }⟩\equiv \epsilon$. C-To with the displayed continuation types the reduct at $B!\epsilon$, exactly the type of the redex.

For $⟨{\ell }_1\mid \mu ⟩\doteq ⟨{\ell }_2\mid \mu ⟩$ with ${\ell }_1\ne {\ell }_2$, rewriting the right row for ${\ell }_1$ skips ${\ell }_2$, chooses fresh $\nu$, and returns $$S_1=[\mu \mapsto ⟨{\ell }_1\mid \nu ⟩],{\epsilon }_3=⟨{\ell }_2\mid \nu ⟩.$$ Since $\mathrm{tail}(\mu )=\mu \in \mathrm{dom}(S_1)$, the guard fails before the recursive equation can recreate the original shape.

For $⟨{\ell }_1\mid \mu ⟩\doteq ⟨{\ell }_2,{\ell }_1\mid \nu ⟩$, rewriting finds the visible ${\ell }_1$ after skipping ${\ell }_2$, returns the identity and residual $⟨{\ell }_2\mid \nu ⟩$, and the tail equation is $\mu \doteq ⟨{\ell }_2\mid \nu ⟩$. Hence the MGU is $[\mu \mapsto ⟨{\ell }_2\mid \nu ⟩]$.

Expose the leftmost $\mathsf{raise}$ on the right. It skips $\mathsf{get}$ and leaves $⟨\mathsf{get},\mathsf{raise}\mid \nu ⟩$. Exposing $\mathsf{get}$ next leaves $⟨\mathsf{raise}\mid \nu ⟩$. The residual equation is therefore $$\mu \doteq ⟨\mathsf{raise}\mid \nu ⟩,$$ so $S=[\mu \mapsto ⟨\mathsf{raise}\mid \nu ⟩]$ is an MGU. Both rows become $⟨\mathsf{raise},\mathsf{get},\mathsf{raise}\mid \nu ⟩$. If $T$ is any other unifier, cancellation of one $\mathsf{raise}$ and one $\mathsf{get}$ gives $T\mu \equiv ⟨\mathsf{raise}\mid T\nu ⟩$. Define $Q$ to agree with $T$ away from $\mu$; then $T=Q\circ S$ on $\mu ,\nu$.

After the inserted request, name the final-return, log, put, and get tails ${\rho }_r,{\rho }_l,{\rho }_p,{\rho }_g$, and write ${\epsilon }_f$ for the single latent row of the lambda-bound callback. Working outward from the return, W solves Thus every sequence has common effect $L_{\mu }=⟨\mathsf{get},\mathsf{put},\mathsf{log}\mid \mu ⟩$, modulo exchange, and ${\epsilon }_f=L_{\mu }$. The wrapper therefore has principal scheme $$\mathrm{\forall }\mu .(\mathbf{1}\stackrel{L_{\mu }}{\to }\mathsf{Int})\stackrel{L_{\mu }}{\to }\mathsf{Int}.$$ Instantiating $\mu \mapsto ⟨\mathsf{raise}\mid \nu ⟩$ gives exactly one $\mathsf{raise}$ in both callback and body: $⟨\mathsf{get},\mathsf{put},\mathsf{log},\mathsf{raise}\mid \nu ⟩$. In the separate let-polymorphic trace, by contrast, the occurrence of $f$ first receives its own fresh instance of the quantified callback tail and W then unifies that instance with the surrounding sequence. The monomorphic parameter has only ${\epsilon }_f$, so its callback and body cannot receive independently quantified row tails. Concretely, the unmodified trace above instantiates the callback’s private $\nu$ with $⟨\mathsf{get},\mathsf{put}\mid \mu ⟩$ and obtains $E_{\mu }=⟨\mathsf{get},\mathsf{put},\mathsf{raise}\mid \mu ⟩$. There $\mathsf{raise}$ comes from the callback scheme; in the present wrapper it comes from instantiating the one shared tail, while the inserted $\mathsf{log}$ is a fixed label of the body.

For the body $\mathsf{perform}\mathsf{ask}()$, W returns $$S_0=\mathsf{id},A_0=\mathsf{Env},{\epsilon }_0=⟨\mathsf{ask}\mid {\mu }_0⟩.$$ Choose fresh $\beta ,\mu$. The return clause $\mathsf{return}x$ reports $\mathsf{Env}!{\delta }_r$; its two solve steps bind $\beta \mapsto \mathsf{Env}$ and ${\delta }_r\mapsto \mu$. The operation clause is inferred under $$u:\mathbf{1},k:\mathsf{Env}\stackrel{\mu }{\to }\mathsf{Env}.$$ Application $kr$ unifies its fresh domain with $\mathsf{Env}$, its fresh result with $\mathsf{Env}$, and its latent row with $\mu$; the two clause-result solves are then identities. The final input equation $$⟨\mathsf{ask}\mid {\mu }_0⟩\doteq ⟨\mathsf{ask}\mid \mu ⟩$$ binds ${\mu }_0\mapsto \mu$. Hence $r:\mathsf{Env}⊢h_r:\mathsf{Env}!\mu$, and the principal computation scheme relative to that context is $\mathrm{\forall }\mu .(\mathsf{Env}!\mu )$. The continuation annotation comes from $k:R_{\mathsf{ask}}\stackrel{\mu }{\to }\beta$: it is the handler output row. Giving it $⟨\mathsf{ask}\mid \mu ⟩$ would incorrectly reintroduce the consumed occurrence on every resumption and would not be a premise of C-Handle.

Set erasure maps both $⟨\mathsf{raise},\mathsf{raise}\mid \nu ⟩$ and $⟨\mathsf{raise}\mid \nu ⟩$ to $\{\mathsf{raise}\}\cup \lfloor \nu \rfloor$. Thus it cannot record that the rethrower consumed one occurrence. If a fallback output tail contains no $\mathsf{raise}$, its input erases to $\{\mathsf{raise}\}\cup \lfloor \nu \rfloor$ and its output to $\lfloor \nu \rfloor$, so ordinary set difference still distinguishes them. The erased handler is nevertheless well typed. For the rethrower, $$E_{\mathrm{in}}\setminus \{\mathsf{raise}\}=\lfloor \nu \rfloor \subseteq \{\mathsf{raise}\}\cup \lfloor \nu \rfloor =E_{\mathrm{out}},$$ which is exactly the target rule’s inclusion premise. What fails is faithful representation: the two source annotations above have the same support, so the target cannot say that exactly one occurrence was consumed. The fallback still changes support and therefore retains that coarser distinction.

Use unique rows with a constrained extension $⟨\ell \mid \mu ⟩$ well formed only under $\ell \notin \mu$. The one-operation handler rule becomes $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e:A!⟨\ell \mid \mu ⟩\\ \ell \notin \mu \\ \mathrm{\Gamma },x:A⊢e_r:B!\mu \\ \mathrm{\Gamma },p:P_{\ell },k:R_{\ell }\stackrel{\mu }{\to }B⊢e_{\ell }:B!\mu \end{array}}{\mathrm{\Gamma }⊢\mathsf{handle}e\mathsf{with}H:B!\mu }.$$ W’s final equation is still ${\epsilon }_0\doteq ⟨\ell \mid \mu ⟩$, but solving it generates and must discharge the predicate $\ell \notin \mu$. A principality proof now needs: sound substitutions for equations and lacks predicates; completeness of solving relative to a stated constraint theory; sound and complete constraint entailment; and factorization of every satisfying substitution through the reported substitution together with a residual constraint set. Ordinary unconstrained MGU factorization is no longer enough.

Take a searched label $\ell$ and a different skipped label $m$: $\epsilon =⟨m,m\mid \rho ⟩$. If $T\epsilon \equiv ⟨\ell \mid \delta ⟩$, the two Rw-Skip steps reduce exposure to $\rho$. Since $\ell \ne m$, cancellation and exchange give a row ${\delta }^{\prime }$ such that $$T\rho \equiv ⟨\ell \mid {\delta }^{\prime }⟩,\delta \equiv ⟨m,m\mid {\delta }^{\prime }⟩.$$ Apply the induction hypothesis to the first equality. If exposure of $\rho$ returns $(S,{\rho }^{\prime })$, there is $Q$ with $T=QS$ on $\rho$ and ${\delta }^{\prime }\equiv Q{\rho }^{\prime }$. Exchange gives $$⟨m,m,\ell \mid Q{\rho }^{\prime }⟩\equiv ⟨\ell ,m,m\mid Q{\rho }^{\prime }⟩,$$ so the residual is $⟨m,m\mid {\rho }^{\prime }⟩$ and the same $Q$ is the factor. Cancellation removes the one exposed $\ell$ but retains both $m$ occurrences. Treating the prefix as a set would collapse them and could not justify this residual equality; multiplicity is used exactly there.

For one operation, inversion supplies declarative body, return, and operation derivations with common output $T\beta !T\mu$ and input $⟨\ell \mid T\mu ⟩$. The body induction hypothesis gives $T=R_0{Q}_0$ after $Q_0=S_0$. The return-clause hypothesis factors through $S_r{Q}_0$; the residual solves $B_r\doteq \beta$ and ${\delta }_r\doteq \mu$. Two applications of MGU factorization produce residuals $R_r^1,R_r$ with $T=R_r{Q}_r$.

Infer the operation clause under $p:P_{\ell },k:R_{\ell }\stackrel{\mu }{\to }\beta$. Its induction hypothesis gives a residual after $S_1{Q}_r$; inversion says it solves $B_1\doteq \beta$ and ${\delta }_1\doteq \mu$. The corresponding MGUs produce $Q_1^1,Q_1^c$ and a residual $R_1$ with $T=R_1{Q}_1^c$. Finally the inverted body premise solves $${\epsilon }_0\doteq ⟨\ell \mid \mu ⟩.$$ Its MGU gives $Q^{\prime }$ and $R^{\prime }$ with $T=R^{\prime }{Q}^{\prime }$. The rules paired with these four stages are respectively the body induction hypothesis, return-clause C-Handle premise, operation-clause premise, and handler-input premise; every equation uses the MGU theorem, so $Q^{\prime }$ is principal.

Let $H_0$ omit $\mathsf{raise}$ and let $H_1$ handle it. If the inner body has effect $⟨\mathsf{raise}\mid \delta ⟩$, forwarding inversion and cancellation force the output of $H_0$ to be equivalent to $⟨\mathsf{raise}\mid {\delta }^{\prime }⟩$. The first root is therefore typed by H-Forward at that same row. Its reduct exposes the request immediately inside $H_1$, whose H-Op premise consumes that occurrence and returns at the outer output row ${\delta }^{\prime }$.

Operationally the nearest-handler decompositions are exactly those in the solution to exercise 25.3; there is no competing outer root. If the final row is $⟨⟩$, progress permits only a return or a step: an exposed $\mathsf{raise}$ would require positive $\mathsf{raise}$-multiplicity in the final row, contradicting its zero multiplicity. Thus forwarding cannot turn a fully handled closed program into an unhandled terminal request.

For unique rows use an exposure judgment $$C⊢\epsilon {\Downarrow }_{\ell }(S,{\epsilon }^{\prime };C^{\prime })$$ whose variable-tail rule chooses fresh $\nu$, returns $S=[\mu \mapsto ⟨\ell \mid \nu ⟩]$, and adds $\ell \notin \nu$ to $C^{\prime }$. Head and skip rules retain and normalize the constraints; every extension carries the well-kindedness premise that its head is absent from its tail. Factorization must say that if $T$ satisfies $C$ and exposes $\ell$, then $T=QS$ on the input variables, $Q$ satisfies $C^{\prime }$, and the target residual is $Q{\epsilon }^{\prime }$.

The one-operation W handler case infers the body and clauses as in the chapter, then solves ${\epsilon }_0\doteq ⟨\ell \mid \mu ⟩$ together with $\ell \notin \mu$. Its result is principal only relative to the residual lacks constraint: every other typed instance factors through the substitution and entails that residual. Duplicate rows avoid precisely this constraint judgment, its entailment theorem, and the constraint component of factorization; their exposure result (25.11) is an ordinary substitution MGU.

Let $$w_0=⟨⟩⟩,w_1=⟨\ell :(m_1,h_1,w_0)\mid w_0⟩⟩,w_2=⟨\ell :(m_2,h_2,w_1)\mid w_1⟩⟩.$$ Selection gives $w_2.\ell =(m_2,h_2,w_1)$. The newest entry therefore yields to $m_2$, not $m_1$, using a clause from $h_2$. Internal safety requires both prompts to be reachable from source-generated handler steps; theorem 31.28 then forbids reusing $m_1$ for the inner prompt. In the displayed $F_{pw}$ perform contraction, the lookup binds $w_2.\ell =(m_2,h_2,w_1)$ but the reduct uses only $m_2$ and $h_2$. The retained third component belongs to the later tail-resumptive optimization, whose $\mathsf{under}$ rules are outside the frozen card.

One suitable type is $$\mathsf{recover}:(1{\to }^{\{\mathsf{raise}\}\cup \beta }A)\to (E{\to }^{\beta \setminus \{\mathsf{raise}\}}A)\to 1{\to }^{\beta }A.$$ The recovery clause checks its handler body under $\phi =\beta \setminus \{\mathsf{raise}\}$. Boolean algebra gives $$\phi \cap \{\mathsf{raise}\}=(\beta \cap \{\mathsf{raise}{\}}^{\mathsf{c}})\cap \{\mathsf{raise}\}{\equiv }_{\mathsf{B}}\varnothing ,$$ which is the Ex-Without premise. A duplicate-row variable $\mu$ may be instantiated by a row containing $\mathsf{raise}$, so it entails no absence. A positive extension $⟨\ell \mid \mu ⟩$ only adds an occurrence; it places no constraint on the tail. The negative property therefore requires the separate Boolean row theory.