Modal Effect Types and Source-to-Met Encodings

Prerequisites. Direct starred prerequisites: Chapter 32; Chapter 25 supplies the row interface used in the first source card. No later core chapter depends on this route.

Consider two library functions that both return unit. A row system might assign $$f:1{\to }^{\mathsf{ask}}1,g:1{\to }^{\varnothing }1,$$ while a capability system makes the authority of $f$ an extra block parameter. The annotations live in different places, but each says how the ambient effect context changes while the function body runs. Writing that change as a modality separates it from the ordinary arrow: $$⟨⟨f⟩{⟩}_{\mathsf{r}}:{◻}_{[\mathsf{ask}]}(1\to 1),⟨⟨g⟩{⟩}_{\mathsf{r}}:{◻}_{[\varnothing ]}(1\to 1).$$ Here $[E]$ discards the current effect context and installs $E$. A relative modality $⟨D⟩$ instead extends the ambient context by $D$: $$[E](F)=E,⟨D⟩(F)=D,F.$$ If the ambient context is $F=\{\mathsf{write}\}$, then $$[\{\mathsf{ask}\}](F)=\{\mathsf{ask}\},⟨\mathsf{ask}⟩(F)=\{\mathsf{ask},\mathsf{write}\}.$$ An absolute modality forgets the ambient permission; an extension modality retains it.

The comparison requires three calculi, not one notation with three spellings.

1. $\mathsf{Met}[\mathcal{T}]$ is the modal target. Its effect structure $\mathcal{T}$ determines equality and inclusion of effect contexts.

2. System $F_{\epsilon }$ is a row-annotated source. Its encoding uses absolute modalities over scoped rows.

3. System $C$ is a capability source with first-class values and second-class blocks. Its encoding uses effect variables and modal boxes over sets.

Both source languages translate to the modal target. There is no translation here from System $F_{\epsilon }$ to System $C$, no translation in the opposite direction, and no claim that either source translation is an inverse.

The modal target

An effect structure $\mathcal{T}$ consists of a kinding relation $\mathrm{\Gamma }⊢D:\mathsf{Eff}$ for finite extensions and an equivalence $\mathrm{\Gamma }⊢D{\equiv }_{\mathcal{T}}{D}^{\prime }$, with well-formedness closed under concatenation. Effect contexts are $$D::=\varnothing \mid \ell ,D\mid ϵ,D,E,F::=\varnothing \mid ϵ\mid D,E.$$ Kinding and equivalence extend componentwise. Subeffecting is derived: $$E{⪯}_{\mathsf{e}}F⟺\mathrm{\exists }D.\mathrm{\Gamma }⊢E,D{\equiv }_{\mathcal{T}}F.$$ Simple rows forbid duplicate labels and identify reorderings. Scoped rows permit duplicates and commute adjacent distinct labels. Sets permit labels and effect variables and quotient by idempotent commutative union. The row encoding uses the scoped-row instance ${\mathcal{R}}_{\mathrm{sc}}$; the capability encoding uses the set instance $\mathcal{S}$.

For progress, the effect structure must satisfy two validity conditions: $$E{⪯}_{\mathsf{e}}\varnothing ⟹E=\varnothing ,\ell {⪯}_{\mathsf{e}}{\ell }^{\prime },E\wedge \ell \ne {\ell }^{\prime }⟹\ell {⪯}_{\mathsf{e}}E.$$ Together they say that a label contained in an effect context occurs there syntactically. The three instances above satisfy both conditions.

The modalities of $\mathsf{Met}[\mathcal{T}]$ are $$\mu ,\nu ::=[E]\mid ⟨D⟩,[E](F)=E,⟨D⟩(F)=D,F.$$ Composition is read from left to right: $$\mu \circ [E]=[E],[E]\circ ⟨D⟩=[D,E],⟨D_1⟩\circ ⟨D_2⟩=⟨D_2,D_1⟩.$$ Thus $(\mu \circ \nu )(E)=\nu (\mu (E))$. The identity is $\mathsf{id}=⟨\varnothing ⟩$.

Kinds distinguish ambient-independent types from arbitrary types: $$K::=\mathsf{Abs}\mid \mathsf{Any}\mid \mathsf{Eff},$$ The only proper subkinding step places $\mathsf{Abs}$ below $\mathsf{Any}$. Every operation parameter and result has kind $\mathsf{Abs}$. Types, terms, contexts, and the principal judgment are Write $\mathrm{\Gamma }⊢A{\equiv }_{\mathsf{Met}}B$ for structural type equivalence and use the same role on modalities; its only non-syntactic premises are the selected effect structure’s ${\equiv }_{\mathcal{T}}$ equations. The complete kinding, equivalence, and context-formation rules are in subappendix A.30. The grammar of $V$ contains complex values: type application and modal elimination may reduce internally while remaining admissible beneath a value-restricted construct. Only this class may appear in modal introduction, modal elimination, and type abstraction. Fix a global operation signature $\mathrm{\Sigma }$. A runtime label context $\mathrm{\Omega }::=\varnothing \mid \mathrm{\Omega },\ell :A⇝B$ records the fresh labels generated by local declarations. The full target judgment is $\mathrm{\Omega }\mid \mathrm{\Gamma }⊢M:A@E$; displays omit the left component when it does not change. The subscript $F$ records the effect context on which a modality acts. Ordinary bindings abbreviate $x{:}_{{\mathsf{id}}_F}A$. The composite $\mathrm{locks}(\mathrm{\Gamma })$ multiplies the locks to the right of a variable. A variable of pure kind crosses every lock; another variable may cross only when its binding modality transforms to that composite.

The modality-transformation judgment $\mathrm{\Gamma }⊢\mu \Rightarrow \nu @F$ has the two characteristic clauses $$\frac{E{⪯}_{\mathsf{e}}\mu (F)}{[E]\Rightarrow \mu @F}\frac{D_1,G{⪯}_{\mathsf{e}}{D}_2,G\text{for every }F{⪯}_{\mathsf{e}}G}{⟨D_1⟩\Rightarrow ⟨D_2⟩@F}.$$ The universal quantifier in the second premise prevents an extension coercion from becoming invalid after ambient subeffecting. Subappendix A.30 prints the selected kinding, variable, modal, operation, handler, and reduction rules.

Modal introduction and elimination have the shapes $$\frac{\mathrm{\Gamma },\mathsf{lock}({\mu }_F)⊢V:A@\mu (F)}{\mathrm{\Gamma }⊢{\mathsf{mod}}_{\mu }V:{◻}_{\mu }A@F}$$ and $$\frac{\mathrm{\Gamma },\mathsf{lock}({\nu }_F)⊢V:{◻}_{\mu }A@\nu (F)\mathrm{\Gamma },x{:}_{(\nu \circ \mu {)}_F}A⊢M:B@F}{\mathrm{\Gamma }⊢{\mathsf{let}}_{\nu }{\mathsf{mod}}_{\mu }x=V\mathsf{in}M:B@F}.$$ Both constructs are value restricted. In particular, ${\mathsf{mod}}_{[\ell ]}(\mathsf{do}\ell ())$ is not a suspension: if arbitrary computations were admitted, it could hide an unhandled request under an empty ambient context.

For an operation $\ell :A^{\prime }⇝B^{\prime }$, a handler clause set is $H=\{\mathsf{return}x\mapsto N,\ell pr\mapsto N^{\prime }\}$. The parameter $\mu$ determines the modal type $r:{◻}_{\mu }(B^{\prime }\to B)$. Its rule requires $\mu \Rightarrow \mathsf{id}@F$ and $\mu \Rightarrow \mu \circ \mu @F$, permitting zero or multiple handler uses. These are hypotheses of the rule, not equations for every modality.

Reduction is call by value. The value normal forms are $$U::=()\mid x\mid \lambda x^A.M\mid \mathrm{\Lambda }{\alpha }^K.V\mid {\mathsf{mod}}_{\mu }U.$$ Figure 2, §3.6, p. 17 of Tang and Lindley [TL26] omits $()$ from this grammar even though unit has no reduction; the displayed grammar makes that necessary case explicit. A local declaration generates a fresh runtime label. Modal beta reduction removes matching introduction and elimination forms. Handler return wraps its result with $\mu \circ ⟨\ell ⟩$; operation handling wraps the reified continuation with $\mu$. If $K$ contains no handler for $\ell$, The side condition makes dispatch choose the dynamically nearest matching handler.

Proof of Theorem 33.2 — Met safety

Source import. This is Tang and Lindley’s Theorems 3.7–3.8, §3.7, p. 18 [TL26]. Their canonical-forms, weakening, substitution, and subeffecting lemmas close the two inductions. The operation case of progress uses validity to recover an occurrence of the stuck label in $E$; the handler-operation case of preservation uses the typed reified continuation. Subappendix D.34 records this imported boundary. ◻

At $E=\varnothing$, validity excludes the request form, so a closed well-typed term either steps or is a value. This is effect safety, not termination.

System $F_{\epsilon }$: the row source

System $F_{\epsilon }$ is a fine-grain call-by-value calculus with scoped rows. Its card is independent of chapter 25’s inference calculus: Rows retain duplicate labels and are equal modulo permutation. The judgments are $\mathrm{\Gamma }{⊢}_{v}V:A$ and $\mathrm{\Gamma }{⊢}_{c}M:A!E$. In particular, $$\frac{\mathrm{\Sigma }(\ell )=A⇝B\mathrm{\Gamma }{⊢}_{v}V:A}{\mathrm{\Gamma }{⊢}_c\mathsf{do}\ell V:B!(\ell ,E)}$$ and a one-operation handler has type $\mathsf{handler}H:((1{\to }^{\ell ,E}A){\to }^{E}A)$. It has no source return clause. The full selected rules appear in subappendix A.30.

Define $⟨⟨-⟩{⟩}_{\mathsf{r}}$ into $\mathsf{Met}[{\mathcal{R}}_{\mathrm{sc}}]$ by translating rows homomorphically and setting Return, let, and type abstraction/application translate homomorphically. The handler translation supplies the missing source return clause and uses a modality-parameterized target handler. For source result type $A$, The annotations $E$ and $\ell ,E$ are part of this type-directed translation.

Proof of Theorem 33.3 — Row-to-Met preservation

Source import. These are Tang and Lindley’s Theorems 4.1–4.2, §4.2, p. 20 [TL26]. The typing induction uses the absolute-modality translation of arrows. The operational induction is on one source step; beta steps take target modal-beta steps, and the handler step uses the translated return and operation clauses. The conclusion is multi-step preservation, not a one-step lockstep simulation. ◻

System $C$: the capability source

System $C$ separates values, second-class blocks, and computations: The judgments $\mathrm{\Gamma }⊢P:T\mid C$ and $\mathrm{\Gamma }⊢M:A\mid C$ track capability sets. A tracked binding $f{:}^{\ast }T$ contributes $\{f\}$; a transparent binding $f{:}^{C}T$ contributes the known set $C$. Blocks are not values unless explicitly boxed. This distinction is a premise of System $C$ safety; the modal target does not recreate it by notation.

The translation into $\mathsf{Met}[\mathcal{S}]$ assigns an effect variable $\hat{f}$ to every tracked capability: A box uses $[⟨⟨C⟩{⟩}_{\mathsf{c}}]$; a block abstraction quantifies its effect variables and uses $⟨\overline{\hat{f}}⟩$. To keep the two target binders visibly distinct, write $\hat{f}$ for the effect variable associated with a tracked source block and $\tilde{f}$ for the term obtained by eliminating that block’s box. The type-directed context translation is The ordinary value clauses are homomorphic. Boxing and the three block clauses are Barred modal lets abbreviate one elimination per block parameter, from left to right. An unmarked elimination uses the identity elimination modality. The remaining non-handler computation clauses make the same discipline explicit: Thus a call first instantiates one quantified effect variable with each actual block’s capability set, then eliminates the resulting extension box.

For the handler, let $H^{f,C}=\{p,r\mapsto N\}$. Its translation is the following binding-sensitive schema: The label ${\ell }_f$ is fresh. The translation instantiates the handled block’s $\hat{f}$ with ${\ell }_f$, passes a boxed operation implementation, and exposes the resumption under $[⟨⟨C⟩{⟩}_{\mathsf{c}}]$. Erasing either binder or the local label changes target scope.

Proof of Theorem 33.4 — Capability-to-Met preservation

Source import. These are Tang and Lindley’s Theorems 5.1–5.2, §5.2, p. 23 [TL26]. Type preservation is simultaneous over value, block, and computation derivations. The block-call case instantiates one effect variable for each actual block argument; the handler case introduces the fresh local operation and types the translated resumption. Semantics preservation is a multi-step simulation on typed configurations because local-label generation changes the runtime instance context. ◻

What the common target does and does not prove

The encodings expose a common shape: They do not establish $F_{\epsilon }{\simeq }_{\mathsf{src}}C$. The domains have different syntax, typing judgments, runtime configurations, and abstraction boundaries. A shared codomain supplies a comparison language; it does not supply a map between the domains.

The 2025 Met paper develops modal effect types and its METL surface language [TWD^+25]. The retained METL artifact implements a bidirectional type checker, interpreter, and paper examples. It does not implement either source-to-Met encoding and is not executable evidence for theorem 33.3, theorem 33.4. The earlier contextual-modal calculus is a separate design, not an earlier name for Met [ZN21].

Capability boxes refine the relation between scope-based capabilities and type-visible boxes, with safety depending on System $C$’s boxing and second-class discipline [BSLBG22]. Locality and effect reflection ask which effects are admitted, reflected, or confined at a boundary [Whi26]; this chapter uses that work only as a comparison card. Modal effect types here are also distinct from dependent multimodal calculi: their contexts carry no dependent modes or mode-morphism substitutions.

Sources.

The target calculus, two source cards, and preservation pairs follow Tang and Lindley [TL26]. The modal design and METL artifact boundary follow Tang et al. [TWD^+25]. The comparison uses System $C$ boxes [BSLBG22], the contextual-modal predecessor [ZN21], and locality/effect reflection [Whi26].