Duplicate-label effect rows and inferred handlers

The exact signature of chapter 25 is The handled labels are distinct. The fixed finite signature satisfies $\mathrm{\Sigma }(\ell )=P_{\ell }⇝R_{\ell }$, with every $P_{\ell },R_{\ell }$ closed and well kinded. Constants have a fixed signature $\mathcal{C}(c)=\mathrm{\forall }\overline{\alpha }\overline{\mu }.A$ whose declarations are closed and well kinded. Row equality is the least congruence generated by $$⟨{\ell }_1,{\ell }_2\mid \epsilon ⟩\equiv ⟨{\ell }_2,{\ell }_1\mid \epsilon ⟩.$$ It has no contraction equation. Substitutions preserve the type and row kinds. Computation and value generalization are

The value and computation judgments are generated by the following complete rules; constants have their declared closed schemes and variable instantiation is kind preserving.

$x:\mathrm{\forall }\overline{\alpha }\overline{\mu }.A\in \mathrm{\Gamma }$$T\text{ instantiates exactly }\overline{\alpha },\overline{\mu }$

$\mathrm{\Gamma }{⊢}_{v}x:TA$

$\mathcal{C}(c)=\mathrm{\forall }\overline{\alpha }\overline{\mu }.A$$T\text{ instantiates exactly }\overline{\alpha },\overline{\mu }$

$\mathrm{\Gamma }{⊢}_{v}c:TA$

$\mathrm{\Gamma },x:A⊢e:B!\epsilon$

$\mathrm{\Gamma }{⊢}_v\lambda x.e:A\stackrel{\epsilon }{\to }B$

$\mathrm{\Gamma }{⊢}_{v}v:A$

$\mathrm{\Gamma }⊢\mathsf{return}v:A!\epsilon$

$\mathrm{\Gamma }{⊢}_v{v}_1:A\stackrel{\epsilon }{\to }B$$\mathrm{\Gamma }{⊢}_v{v}_2:A$

$\mathrm{\Gamma }⊢v_1{v}_2:B!\epsilon$

$\mathrm{\Gamma }⊢e_1:A!\epsilon$$\mathrm{\Gamma },x:A⊢e_2:B!\epsilon$

$\mathrm{\Gamma }⊢e_1\mathsf{to}x.e_2:B!\epsilon$

$\mathrm{\Sigma }(\ell )=P_{\ell }⇝R_{\ell }$$\mathrm{\Gamma }{⊢}_{v}v:P_{\ell }$

$\mathrm{\Gamma }⊢\mathsf{perform}\ell v:R_{\ell }!⟨\ell \mid \epsilon ⟩$

$\mathrm{\Gamma }⊢e_1:A!⟨⟩$$\overline{a}=\mathrm{ftv}(A)\setminus \mathrm{ftv}(\mathrm{\Gamma })$$\mathrm{\Gamma },x:\mathrm{\forall }\overline{a}.A⊢e_2:B!\epsilon$

$\mathrm{\Gamma }⊢\mathsf{let}x=e_1\mathsf{in}{e}_2:B!\epsilon$

$\mathrm{\Gamma }⊢e:A!\epsilon$$\epsilon \equiv {\epsilon }^{\prime }$

$\mathrm{\Gamma }⊢e:A!{\epsilon }^{\prime }$

$\mathrm{\Gamma }⊢e:A!⟨{\ell }_1,\dots ,{\ell }_n\mid \epsilon ⟩$$\mathrm{\Gamma },x:A⊢e_r:B!\epsilon$$(\mathrm{\Sigma }({\ell }_i)=P_i⇝R_i{)}_{i=1}^n$$(\mathrm{\Gamma },p_i:P_i,k_i:R_i\stackrel{\epsilon }{\to }B⊢e_i:B!\epsilon {)}_{i=1}^n$

$\mathrm{\Gamma }⊢\mathsf{handle}e\mathsf{with}H:B!\epsilon$

Rows in common premises may be replaced by equivalent rows.

Evaluation and handler-free request contexts are Reduction is closed under $E$. Its complete roots are For the nearest syntactic handler, whose body context $R$ contains no handler frame, where the first rule requires ${\ell }_i\in \mathsf{handled}(H)$ and the second requires $\ell \notin \mathsf{handled}(H)$. These tests are complementary; forwarding crosses exactly one handler layer.

Row exposure is the partial operation $\mathsf{rewrite}(\epsilon ,\ell )=(S,{\epsilon }^{\prime })$ defined by with fresh $\nu$; rewriting $⟨⟩$ fails. It satisfies $S\epsilon \equiv ⟨\ell \mid S{\epsilon }^{\prime }⟩$. The complete unifier first applies reflexivity and variable binding, then uses The same-kind clash cases, tried after reflexivity and variables, are A type–row equation is rejected as ill kinded before unification; U-Var fails its occurs check. Arrows solve domain, effect, then codomain: $$\begin{array}{c}{S}_1=\mathsf{U}(A_1,A_2),S_2=\mathsf{U}(S_1{\epsilon }_1,S_1{\epsilon }_2),\\ S_3=\mathsf{U}(S_2{S}_1{B}_1,S_2{S}_1{B}_2),\\ \mathsf{U}(A_1\stackrel{{\epsilon }_1}{\to }{B}_1,A_2\stackrel{{\epsilon }_2}{\to }{B}_2)=S_3{S}_2{S}_1.\end{array}$$ For $\mathsf{U}(⟨\ell \mid {\epsilon }_1⟩,{\epsilon }_2)$ expose $(S_1,{\epsilon }_3)$ on the right, reject when $\mathrm{tail}({\epsilon }_1)\in \mathrm{dom}(S_1)$, solve $S_2=\mathsf{U}(S_1{\epsilon }_1,S_1{\epsilon }_3)$, and return $S_2{S}_1$.

Inference reports ${\mathsf{W}}_v(\mathrm{\Gamma },v)=(S,A)$ and ${\mathsf{W}}_c(\mathrm{\Gamma },e)=(S,A,\epsilon )$. Variables instantiate every quantifier. If $\mathcal{C}(c)=\mathrm{\forall }\overline{\alpha }\overline{\mu }.A$, the constant case replaces the displayed quantifiers by fresh variables through $T$, and returns $(\mathsf{id},TA)$. A lambda infers its body under a fresh monotype. The computation clauses are, in source order:

1. return a value and a fresh row variable;

2. infer both application values and unify the operator with $A\stackrel{\mu }{\to }\alpha$;

3. infer both sides of sequencing and unify their effects;

4. infer an operation parameter, unify it with $P_{\ell }$, and return $R_{\ell }!⟨\ell \mid \mu ⟩$;

5. infer a let-bound computation, unify its effect with $⟨⟩$, generalize its value type, and infer the body;

6. for a handler, infer the body as $(S_0,A_0,{\epsilon }_0)$, choose fresh $\beta ,\mu$, and accumulate substitutions through the return clause and every operation clause. Each clause result is unified first with $\beta$ and then with $\mu$; clause $i$ is inferred under $p_i:P_i$ and $k_i:R_i\stackrel{\mu }{\to }\beta$. Finally unify ${\epsilon }_0$ with $⟨{\ell }_1,\dots ,{\ell }_n\mid \mu ⟩$ and report $\beta !\mu$ after the accumulated substitution.

Here is the exact handler accumulator. For a current substitution $Q$, put $$R=\mathsf{U}(QX,QY),\mathrm{solve}(Q;X\doteq Y)=R\circ Q.$$ Choose fresh $\beta ,\mu$, compute $(S_0,A_0,{\epsilon }_0)={\mathsf{W}}_c(\mathrm{\Gamma },e)$, and set $Q_0=S_0$. Infer the return clause and compose its local substitution before solving its two outputs: $$\begin{array}{c}(S_r,B_r,{\delta }_r)={\mathsf{W}}_c(Q_0\mathrm{\Gamma },x:Q_0{A}_0,e_r),Q_r^0=S_r{Q}_0,\\ Q_r^1=\mathrm{solve}(Q_r^0;B_r\doteq \beta ),Q_r=\mathrm{solve}(Q_r^1;{\delta }_r\doteq \mu ).\end{array}$$ Starting with $Q_0^c=Q_r$, process operation clauses in source order: Finally set $$Q^{\prime }=\mathrm{solve}(Q_n^c;{\epsilon }_0\doteq ⟨{\ell }_1,\dots ,{\ell }_n\mid \mu ⟩)$$ and return $(Q^{\prime },Q^{\prime }\beta ,Q^{\prime }\mu )$. Every recursive inference call receives the environment after the current substitution; every displayed result is likewise fully substituted.

Generalized-evidence and exclusion cards

The generalized-evidence source and intermediate use Evidence extension and selection satisfy $$⟨\ell :q\mid w⟩⟩.\ell =q,⟨{\ell }^{\prime }:q\mid w⟩⟩.\ell =w.\ell (\ell \ne {\ell }^{\prime }).$$ A prompt evaluates its body under $⟨\ell :(m,h,w)\mid w⟩⟩$. An operation for label $\ell$ selects $w.\ell =(m,h,w^{\prime })$, selects its clause from $h$, and yields to $m$. Only internal-safe terms generated from source terms may contain prompt, yield, or markers.

The monadic target has ordinary higher-kinded polymorphic lambda terms and $$\mathsf{Mon}\epsilon A=\mathsf{Evv}\epsilon \to \mathsf{Ctl}\epsilon A.$$ The translation judgment is $\mathrm{\Gamma }⊢e:\sigma \mid \epsilon ⇝e^{\prime }$. Its representative clauses are Here $▹$ is the target control-monad bind: $e▹g$ runs $e$ under the current evidence vector, passes a $\mathsf{Pure}$ result to $g$, and extends the resumption of a $\mathsf{Yield}$. The omitted type parameters are the explicit source annotations shown in Figure 5 and Figure 11 (Appendix E, “Full rules”) of the version-4 report [XL21]; this card does not reconstruct them by inference.

For effect exclusion, fix a finite universe $\mathcal{U}$ and Boolean effect formulas $$\phi ::=\beta \mid \varnothing \mid \{F\}\mid {\phi }^{\mathsf{c}}\mid \phi \cup \phi \mid \phi \cap \phi .$$ The source uses a $T$-prefix; this appendix renames it to $\mathsf{Ex}$ to avoid collision with the adjacent tunnelling and System-$\mathsf{Xi}$ cards. The local runtime interface is Configurations are $⟨e\mid k⟩$; $\tau {⊢}_{k}k\setminus \phi$ types a stack and ${⊢}_m⟨e\mid k⟩\mathsf{ok}$ types a configuration. The characteristic typing, stack, and machine rules are

$\mathrm{\Gamma }{⊢}_{\complement }e:\tau \mid \phi$$\phi \cap \{F\}{\equiv }_{\mathsf{B}}\varnothing$

$\mathrm{\Gamma }{⊢}_{\complement }e\mathsf{without}F:\tau \mid \phi$

$\tau {⊢}_{k}k\setminus \phi$

$\tau {⊢}_k([]\mathsf{without}F)::k\setminus (\phi \cup \{F\})$

$\cdot {⊢}_{\complement }e:\tau \mid {\phi }_1$$\tau {⊢}_{k}k\setminus {\phi }_2$${\phi }_1\cap {\phi }_2{\equiv }_{\mathsf{B}}\varnothing$

${⊢}_m⟨e\mid k⟩\mathsf{ok}$

The machine step for $\mathsf{do}F(v)$ has the side condition $F\notin \mathsf{forb}(k)$. Pushing a $\mathsf{without}F$ expression creates the displayed forbid frame; a returned value pops it. There is no subeffecting rule.