ch:modal-effect-types: ch:modal-effect-types

Replacement gives $[\{\mathsf{write}\}](F)=\{\mathsf{write}\}$. Extension gives $⟨\mathsf{write}⟩(F)=\{\mathsf{write},\mathsf{read}\}$. Composition is left to right, so $([\{\mathsf{write}\}]\circ ⟨\mathsf{read}⟩)(F)=\{\mathsf{read},\mathsf{write}\}$. The latter two retain $\mathsf{read}$; absolute replacement alone does not.

Progress may classify $K[\mathsf{do}\ell U]$ as normal at $\varnothing$, because its definition asks only for $\ell {⪯}_{\mathsf{e}}\varnothing$. The usual empty-effect corollary can no longer remove that alternative, so the term can be stuck on an unhandled request. This countermodel attacks the corollary from progress; it does not contradict the separately stated preservation conclusion.

Left-to-right composition gives $[E]\circ ⟨\ell ⟩=[\ell ,E]$. The return variable has type ${◻}_{[\ell ,E]}A$; the resumption has type ${◻}_{[E]}(B^{\prime }\to B)$. The handler rule additionally requires $[E]\Rightarrow \mathsf{id}@F$ and $[E]\Rightarrow ([E]\circ [E])@F$. Since $[E]\circ [E]=[E]$, both obligations reduce to the absolute-modality transformation premises at $F$.

The source function translates to $${\mathsf{mod}}_{[\ell ,E]}(\lambda x^{⟨⟨A⟩{⟩}_{\mathsf{r}}}.\mathsf{do}\ell x):{◻}_{[\ell ,E]}(⟨⟨A⟩{⟩}_{\mathsf{r}}\to ⟨⟨B⟩{⟩}_{\mathsf{r}}).$$ Its application to $V$ is $$\mathsf{let}{\mathsf{mod}}_{[\ell ,E]}f=⟨⟨{\lambda }^{\ell ,E}x.M⟩{⟩}_{\mathsf{r}}\mathsf{in}f⟨⟨V⟩{⟩}_{\mathsf{r}}.$$ The absolute box runs the body at exactly $\ell ,E$. Replacing it by $⟨\ell ⟩$ would retain every ambient effect, so it would not encode the source arrow’s exact row.

Writing $T=1\Rightarrow 1$, the translated block begins $$\mathrm{\Lambda }\hat{f}.{\mathsf{mod}}_{⟨\hat{f}⟩}(\lambda x^1.\lambda f^{{◻}_{[\hat{f}]}⟨⟨T⟩{⟩}_{\mathsf{c}}}.\mathsf{let}{\mathsf{mod}}_{[\hat{f}]}\tilde{f}=f\mathsf{in}\tilde{f}x).$$ Thus the formal capability becomes an effect variable, the block body is boxed by an extension modality, its block argument is boxed absolutely at that effect variable, and elimination records the same absolute modality on the hatted callable variable.

Typing uses the binding freshness convention when M-Local extends the local signature: ${\ell }_f$ must avoid the translated context so that substituting it for $\hat{f}$ captures no pre-existing label. This is alpha-freshness of the local binder, not an extra side condition on the rule. Operational preservation uses freshness when the generated runtime instance context extends with one new label and when substitution identifies the tracked effect variable with that unique label. Reusing an active label aliases two dynamic instances; the instance-context extension and local-label case would then lose their inversion premise even if the signatures agree.

Write $H_{\mathrm{r}}=\mathsf{handler}\{\mathsf{ask}pr\mapsto \mathsf{return}p\}$. Its row translation is The handled thunk has type ${◻}_{[\mathsf{ask}]}(1\to 1)$; its absolute box is the source row. The row proof uses that ${\mathcal{R}}_{\mathrm{sc}}$ retains duplicate labels while commuting adjacent distinct labels, so the handler case removes the selected occurrence without contracting the residual row.

For the System-$C$ term, let $G$ translate the body after abstracting the tracked block: Its handler translation has the modal skeleton Here $\hat{f}$, $⟨\hat{f}⟩$, $[{\ell }_f]$, and ${\ell }_f$ are respectively the quantified effect variable, extension modality, absolute box on the operation implementation, and fresh runtime label. The capability proof uses freshness of ${\ell }_f$ and simultaneous preservation for blocks and computations; neither premise is supplied by the row proof. Both source terms return unit after one handled request, but their target terms are related only by this chosen observation, not by a proved source equivalence.

The proved span is $$F_{\epsilon }⟶\mathsf{Met}[{\mathcal{R}}_{\mathrm{sc}}],C⟶\mathsf{Met}[\mathcal{S}].$$ The first domain has duplicate-preserving rows and first-class functions; the second has sets and second-class blocks. Their steps also use different runtime configurations. A source-to-source compiler would require an explicit term and type translation plus a relation between observations and a forward simulation (or another operational-correctness argument). Neither target translation supplies an inverse with which to manufacture these data.

Introduction checks the identity function under $\mathsf{lock}([E{]}_F)$ at $E$, yielding ${\mathsf{mod}}_{[E]}(\lambda x.x):{◻}_{[E]}(A\to A)@F$. Elimination with outer modality $\mathsf{id}$ binds $h{:}_{[E{]}_F}(A\to A)$. Using $h$ after no further lock requires $[E]\Rightarrow \mathsf{id}@F$. If $h$ instead has a type of pure kind, M-Aux-Abs discharges the auxiliary premise of M-Var without a modality transformation.

For application, the induction hypotheses type the function at ${◻}_{[E]}(A\to B)$ and the argument at $A$. Rule M-LetMod eliminates the box, after which ordinary application yields $B@E$.

For the handler, the translated thunk has ${◻}_{[\ell ,E]}(1\to A)$, its returned value has ${◻}_{[\ell ,E]}A$, and its resumption has ${◻}_{[E]}(B^{\prime }\to A)$, matching the translation of the source continuation arrow. A source handled-request step substitutes the parameter and rehandled continuation. The target first performs modal beta, then the Met operation step, and finally modal beta in the translated clause; the resulting term is the translation of the source reduct. This is a nonempty finite sequence, as required by the ${⟶}^{\ast }$ conclusion.

The simultaneous hypotheses translate values, blocks, and computations. In the block case, introduce one effect variable ${\hat{f}}_j$ per formal block, box the function under $⟨\overline{\hat{f}}⟩$, and eliminate each formal’s $[{\hat{f}}_j]$ box before applying the computation hypothesis. In the call case, if actual $Q_j$ has capability set $C_j$, instantiate ${\hat{f}}_j:=⟨⟨C_j⟩{⟩}_{\mathsf{c}}$. The target result type is then $⟨⟨B⟩{⟩}_{\mathsf{c}}[⟨⟨C_j⟩{⟩}_{\mathsf{c}}/{\hat{f}}_j]$, equal by the translation-substitution lemma to $⟨⟨B[C_j/f_j]⟩{⟩}_{\mathsf{c}}$. Eliminating the relative box places the call at the union of the callee and actual capability effects.

1. Theorem 33.2 plus the first validity condition proves the claim.

2. No theorem proves it. The two translations form a span, and neither has a proved inverse.

3. The claim fails because the METL artifact implements neither source translation; an implementation may pass its own examples while a proposed System-$C$ encoder mishandles a block call.

4. The claim fails because effect safety constrains stuck requests. Ownership noninterference constrains observations. Two safe programs may write different public values.