Scoped Operations and Explicit Substitution

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

The transaction from chapter 22 performs a write and may raise an exception. Treat $\mathsf{transaction}(M)$ as a scoped operation: effects of $M$ commit on return and roll back on failure, while a computation sequenced after the transaction lies outside the rollback region. Put $$M:=\mathsf{put}(s_0+1)\gg =\lambda \mathrm{\_}.\mathsf{return}(),k:=\lambda \mathrm{\_}.\mathsf{raise}(e_0).$$ The first-order algebraicity equation from the previous chapter would force $$\mathsf{transaction}(M)\gg =k\stackrel{?}{=}\mathsf{transaction}(M\gg =k).$$ The two sides do not have the same transactional boundary. On the left, $M$ returns, the write is committed, and only then does $k$ raise outside the transaction; the store visible with the failure is $s_0+1$. On the right, the same raise has been moved into the transaction body, so failure rolls the write back and exposes $s_0$. Equation (23.1) has turned a continuation into part of the scope.

The running example makes the same defect visible without state. Let $\mathsf{or}$ be nondeterministic choice and let $\mathsf{once}$ select the first solution. With $k(x)=\mathsf{or}(x,x+1)$, the intended calculation is If $\mathsf{once}$ were algebraic, bind would instead be pushed into its argument: The problem is therefore structural, not a missing effect equation. An ordinary algebraic node stores parameters and response branches. A scoped node must additionally say which computation belongs to the scope and which computation follows it. The latter must remain outside when a later bind is performed.

We therefore freeze the syntax and construct its substitution directly.

The scoped signature

The source calculus separates ordinary algebraic operations from operations that own computations. A general functorial signature has a polynomial presentation that names the parameters and branches used in calculations.

This polynomial presentation names parameters and branches for nondeterminism, exceptions, local state, and concurrency.

The double occurrence $T(TA)$ in the scope constructor is the essential one. A return from a computation inside a scope need not be a final $A$-value. It may instead be an entire $TA$-computation representing what should happen after the scope closes. That extra layer is the explicit substitution: the inside return supplies the input to the continuation that follows the scope.

The nested shape is $$\mathsf{Var}a,\mathsf{Op}(\mathrm{\Sigma }(TA)),\mathsf{Scope}(\mathrm{\Gamma }(T(TA))).$$

Proof of Proposition 23.3 — Existence for the finitely branching running signatures

Proof. Under the stated hypotheses, every response and owned-position set displayed below is finite. Parameter sets may be arbitrary: they occur only as coefficients of sums and products. Hence $\mathrm{\Sigma }$ and $\mathrm{\Gamma }$ are finitary polynomial functors: they preserve injections and colimits of $\omega$-chains of injections. Starting from the empty endofunctor, induction on $n$ shows that every connecting map $T_n\to T_{n+1}$ is componentwise injective; sums, finite products, finite powers, and the composite $T_n(T_n-)$ preserve that property. At the limit, the nested summand uses the diagonal cofinality calculation $$\underset{n}{\mathrm{colim}}{T}_n(T_{n}A)\cong \underset{(m,n)\in {\mathbb{N}}^2}{\mathrm{colim}}{T}_m(T_{n}A)\cong (\underset{m}{\mathrm{colim}}{T}_m)((\underset{n}{\mathrm{colim}}{T}_n)A).$$ For the first isomorphism, every pair $(m,n)$ maps to a diagonal stage $(N,N)$ with $N\ge m,n$; for the second, finitarity of each stage moves the inner colimit through $T_m$, after which the outer colimit is taken. Finitarity of $\mathrm{\Sigma }$ and $\mathrm{\Gamma }$ now gives $\mathcal{G}({\mathrm{colim}}_n{T}_n)\cong {\mathrm{colim}}_n\mathcal{G}(T_n)$, so $T={\mathrm{colim}}_n{T}_n$ is the initial algebra for the $\mathsf{once}$, finite-exception, and finite-local-state signatures. ◻

Three running signatures

For nondeterminism with $\mathsf{fail}$, binary $\mathsf{or}$, and unary $\mathsf{once}$, take $$\mathrm{\Sigma }X\cong 1+X\times X,\mathrm{\Gamma }X\cong X.$$ The two summands of $\mathrm{\Sigma }$ are the nullary and binary algebraic nodes; $\mathsf{once}$ owns one scoped computation.

For exceptions from a set $E$, the source gives $$\mathrm{\Sigma }X\cong E,\mathrm{\Gamma }X\cong X\times X^E.$$ The ordinary operation is raise: an exception value is a parameter and there is no response branch. A scoped catch node owns one protected computation and one recovery computation for each exception. All those computations return the same intermediate result type; an outside continuation remains separate.

For local state with names $N$ and stored values $S$, take so the ordinary signature and scoped part are $$\mathrm{\Sigma }X\cong N\times X^S+(N\times S)\times X,\mathrm{\Gamma }X\cong N\times S\times X.$$ A get node chooses one continuation branch from the stored value it receives; a put node carries a name and new value and has one unit-response branch. A local node has two ordinary parameters, a name and its initial value, and exactly one scoped computation. Its interpretation belongs to the source’s later semantic development and is not part of this syntax chapter.

The explicit substitution hidden in a scope node

The nested constructor is compact but conceals the three pieces that the opening calculation requires. Exposing them does not change the syntax.

Fix a polynomial scoped symbol $s\in \mathcal{S}$. A scope node returning $A$ may be represented by data $$p:P_s,X:\mathbf{Set},m:Q_s\to TX,k:X\to TA.$$ We write this representative as $${\mathsf{Scope}}_s(p;X;m;k).$$ The roles are distinct: The intermediate set $X$ is not observable syntax. Replacing its names must not create a different node.

Equation (23.12) says that an intermediate return can be renamed either before leaving the scope or in the explicit continuation. No handler or categorical representation theorem is being imported.

Proof of Lemma 23.5 — Canonical nested representative

Proof. First check that $\mathsf{pack}$ respects one generating reindexing. The two representatives in (23.12) map at position $q$ to Hence $\mathsf{pack}$ is well defined on classes.

For $u:Q_s\to T(TA)$, $$\mathsf{pack}(\mathsf{unpack}(u))(q)\stackrel{(23.13)}{=}T({\mathsf{id}}_{TA})(u(q))\stackrel{\text{functor identity}}{=}u(q).$$ Conversely, instantiate (23.12) with $h=k:X\to TA$ and $k^{\prime }={\mathsf{id}}_{TA}$: $$[X,m,k]\stackrel{(23.12)}{=}[TA,\lambda q.Tk(m(q)),{\mathsf{id}}_{TA}]\stackrel{(23.13)}{=}\mathsf{unpack}(\mathsf{pack}[X,m,k]).$$ Thus the maps are inverse. ◻

This lemma is the bridge between the readable representation (23.10) and the exact nested constructor.

Every stage functor preserves injections, so the least stage containing a representative is a well-founded rank. At a successor stage, unpack the scope and apply the rank hypotheses to its owned computations and continuation.

Proof of Lemma 23.6 — Well-founded elementwise recursion

Proof. Use the monic convergent transfinite initial chain of $\mathcal{G}$ fixed in definition 23.2. Its first stages are $$T_{0}A=0,T_{\alpha +1}A=A+\mathrm{\Sigma }(T_{\alpha }A)+\mathrm{\Gamma }(T_{\alpha }(T_{\alpha }A)),$$ and a limit stage is the colimit of the preceding stages. The connecting maps are componentwise injective by hypothesis. A transfinite induction shows that every stage functor preserves injections. At a successor, this follows because sums and the polynomial functors $\mathrm{\Sigma },\mathrm{\Gamma }$ preserve injections and because the nested composite $T_{\alpha }(T_{\alpha }-)$ does so when $T_{\alpha }$ does. At a limit $\lambda$, the stage is the pointwise colimit of the earlier chain. Suppose classes represented by $x\in T_{\alpha }A$ and $y\in T_{\beta }A$ have equal images under an injection $i:A\to B$. Equality in the chain colimit is witnessed at some above $\alpha$ and $\beta$: the transported elements have equal images under $T_{\gamma }i$. Injectivity of $T_{\gamma }i$ makes the transported representatives equal, hence the original colimit classes are equal. Thus the limit stage also preserves injections. Since the connecting maps are monic, we may identify each stage with its image in the next one. At the convergence ordinal, the colimit is $T$ by the stated construction hypothesis.

Proceed by induction on the least stage containing the term. The same least-stage argument gives the following recursion schema. Given result sets $D_A$ and clauses with the scoped clause invariant under reindexing, define $F_A(t)$ at the least stage of $t$ by the corresponding clause. At a successor stage all displayed recursive arguments lie at an earlier stage; at a limit, the term already has a representative at an earlier stage. The connecting maps are injective, so a term cannot acquire a different constructor when transported to a later stage, and using the unique least stage makes the value independent of a later-stage presentation. Reindexing invariance makes it independent of the chosen elementwise representative. This constructs $F$; induction on least stage proves that it is the unique family satisfying the three clauses. ◻

Proof of Corollary 23.7 — Elementwise induction

Proof. Use the well-founded rank constructed in lemma 23.6.

Variables and ordinary nodes give the first two induction clauses directly. A scope introduced at stage $\alpha +1$ has, in the $s$-summand, parameters $p:P_s$ and a family $$u:Q_s\to T_{\alpha }(T_{\alpha }A).$$ Take $X:=T_{\alpha }A$, take $m(q)$ to be $u(q)$ followed by the stage inclusion into $TX$, and take $k:X\to TA$ to be the stage inclusion. Then every $m(q)$ and every $k(x)$ comes from stage $\alpha$, so the induction hypotheses give the premises of the scoped clause in (23.14). A term at a limit stage already appears at an earlier stage. Finally, because $\mathcal{P}$ respects (23.12), the conclusion is independent of the chosen elementwise representative. ◻

The failed substitution and the hard repair

For an ordinary algebraic operation, substitution must recurse into every response branch. With elementwise notation, $${\mathsf{Op}}_o(p,k),k:R_o\to TA,$$ so a substitution $f:A\to TB$ naturally sends $k(r)$ to $k(r)[f]$. From this point onward, $t[f]$ is postfix Kleisli substitution: its second argument is a map $f:A\to TB$. The notation deliberately resembles ordinary postfix substitution, but the displayed type distinguishes the two uses.

One tempting generic traversal copies that pattern into the owned computation while also preserving the explicitly stored continuation position: $${\mathsf{Scope}}_s(p;X;m;k)\stackrel{\text{bad}}{\mapsto }{\mathsf{Scope}}_s(p;X;\lambda q.m(q)[f];\lambda x.k(x)[f]).$$ Call this the all-fields traversal. In general, (23.16) is not even typed. Applying the substitution to $m(q):TX$ first requires $X=A$. Even under that equality, the transformed body has type $TB$, so the new scope carrier would have to be $B$, whereas the transformed old continuation is still indexed by $x:A$. Without a further adapter it has the required domain only when $A=B$. Thus the clause is typed in the endomorphic homogeneous special case $X=A=B$; there it duplicates the post-computation by moving it into the scope and retaining it after the scope. This is distinct from false algebraicity, which moves the post-computation into the scoped body and thereby loses it from the outside continuation. For the smart node $\mathsf{once}(t)={\mathsf{Scope}}_{\mathsf{once}}(\ast ;A;\lambda \mathrm{\_}.t;\mathsf{Var})$, the three results are The opening calculation exhibits the second result; (23.16) specifies the third. A scoped computation and an outer continuation are different recursive positions.

The third line is the repair. It is also the reason explicit substitution was needed: the continuation is present as syntax and can be composed without pretending that it lies inside the scope.

Proof of Lemma 23.10 — Substitution respects reindexing

Proof. For any representative $[X,m,k]$, form the candidate $$C_f[X,m,k]:=[X,m,\lambda x.k(x)[f]],$$ where the substitutions in the continuation are already defined by the least-stage recursion. We show that $C_f$ is constant on each generating reindexing (23.12). Put $$k_f^{\prime }(y):=k^{\prime }(y)[f].$$ For the left representative, For the right representative, $$C_f[Y,\lambda q.Th(m(q)),k^{\prime }]\stackrel{\text{definition}}{=}[Y,\lambda q.Th(m(q)),k_f^{\prime }].$$ These two candidates are related by (23.12), now with continuation $k_f^{\prime }$. Hence $C_f$ descends through the generated congruence. On every stage-bounded representative used in definition 23.9, the descended map is exactly the scoped recursive clause in (23.17). Therefore the recursively constructed substitution has the displayed value on every representative and is independent of the chosen representative. ◻

Consequently the candidate is independent of the chosen representative, so equation 23.17 defines substitution on every reindexing class.

The canonical nested clause follows rather than being guessed. Define $b_f:TA\to TB$ by $b_f(u)=u[f]$. A canonical representative $[TA,u,\mathsf{id}]$ becomes $[TA,u,b_f]$ by (23.17). Canonicalizing it with lemma 23.5 gives $$\mathsf{Scope}(v)[f]=\mathsf{Scope}(\mathrm{\Gamma }(T{b}_f)(v)).$$ This is exactly the source implementation $$\mathsf{Scope}sc\gg =f=\mathsf{Scope}(\mathsf{fmap}(\mathsf{fmap}(\gg =f))sc).$$ The inner map traverses the scoped syntax only to reach its returned explicit continuations; it does not move $f$ underneath the scoped boundary as (23.16) does.

Ordinary and genuinely scoped calculations

For nondeterminism, define Then ordinary substitution is the familiar algebraic calculation:

Now make the continuation explicit in the unary scoped node: $$\mathsf{once}(t;k):={\mathsf{Scope}}_{\mathsf{once}}(\ast ;X;\lambda \mathrm{\_}.t;k),t:TX,k:X\to TA.$$ The ordinary smart constructor is $\mathsf{once}(t)=\mathsf{once}(t;\mathsf{Var})$. Hence The body $t$ is byte-for-byte the same syntax in both lines. Only the explicit continuation changes.

For a concrete comparison, let $$t=\mathsf{or}(\mathsf{Var}(1),\mathsf{Var}(5)),f(x)=\mathsf{or}(\mathsf{Var}(x),\mathsf{Var}(x+1)).$$ Then the three candidate clauses produce The correct clause keeps the two original branches inside the scope and puts $f$ only in the outside continuation. False algebraicity moves $f$ into the owned computation and loses it outside. The all-fields traversal both moves and retains it, duplicating the post-computation.

Exceptions display both ordinary and scoped clauses. Define where $M:TX$, $H:E\to TX$, and $$m(\mathsf{inl}(\ast ))=M,m(\mathsf{inr}(e))=H(e).$$ For $f:A\to TB$, the complete substitution calculations are The exception value $e$ is an ordinary parameter. The protected computation $M$ and every recovery computation $H(e)$ are owned by the catch scope. Only the continuation after catch is composed with $f$.

Local state makes all three roles visible at once. Write $$\mathsf{local}(n,s,t;k):={\mathsf{Scope}}_{\mathsf{local}}((n,s);X;\lambda \mathrm{\_}.t;k).$$ Then The name $n$ and initial state $s$ are ordinary parameters, the computation $t$ is owned by the local scope, and $k$ is the only component composed with the later substitution.

Substitution equations and the monad

The construction is useful only if repeated explicit substitutions compose as ordinary substitution should. We prove this directly on the elementwise signature; no semantic interpretation is involved.

Proof of Theorem 23.11 — Explicit-substitution equations

Proof. Equation (23.22a) is the first defining clause of definition 23.9. For (23.22b), apply corollary 23.7 to the family $${\mathcal{P}}_Z(u)⟺u[{\eta }_Z]=u.$$ For (23.22c), define $${\mathcal{Q}}_Z(u)⟺\mathrm{\forall }B,C,f:Z\to TB,g:B\to TC.(u[f])[g]=u[(\lambda z.f(z)[g])].$$ Both families respect reindexing because substitution is well defined by lemma 23.10. The variable case of $\mathcal{P}$ is $$\mathsf{Var}(z)[{\eta }_Z]={\eta }_Z(z)=\mathsf{Var}(z)$$ by the variable clause and the definition of ${\eta }_Z$. At an ordinary node, function extensionality and the induction hypotheses on every response branch give At a scoped node, the scoped computations are not traversed: This proves (23.22b).

For (23.22c), apply the induction just described to $\mathcal{Q}$, and then instantiate its universal quantifiers with the displayed $B,C,f,g$. The variable case is $\mathsf{Var}(a)[f][g]=f(a)[g]=h(a)=\mathsf{Var}(a)[h]$ by the variable clause. The ordinary case is The scoped case is the load-bearing one: The body $m$ is unchanged on all four lines. By lemma 23.10, the calculation descends from representatives to reindexing classes. ◻

Proof of Corollary 23.12 — Scoped-syntax monad

Proof. Left and right unit are (23.22a) and (23.22b). Associativity is (23.22c). In each case, expand (23.23). ◻

The functorial renaming already present in the exact nested construction is not a second, unrelated traversal.

Proof of Lemma 23.13 — Renaming is return substitution

Proof. For each set $Z$, let ${\mathcal{R}}_Z(u)$ assert (23.25) for every set $W$ and every map $r:Z\to W$. This family respects reindexing because both the functor action and substitution are well defined on the quotient. Apply corollary 23.7 to $\mathcal{R}$ and then instantiate it with the displayed $r:A\to B$. The variable case is $$Tr(\mathsf{Var}(a))=\mathsf{Var}(r(a))=\mathsf{Var}(a)[\mathsf{Var}\circ r],$$ by the functor and variable-substitution clauses. At an ordinary node, both sides preserve the parameter and apply the respective action pointwise to every response branch, so function extensionality applied to the induction hypotheses equates the resulting branch functions.

For a scoped representative $[X,m,k]$, first compute the source functor action through its canonical nested representative. Packing gives the body $q\mapsto Tk(m(q))$. Applying $Tr$ to the outer result applies $T(Tr)$ to that body, hence Unpacking and (23.12) therefore give the renamed node $[X,m,(Tr)\circ k]$. Substitution by $\mathsf{Var}\circ r$ gives instead $$[X,m,\lambda x.k(x)[\mathsf{Var}\circ r]],$$ and the induction hypothesis on each continuation branch gives $$k(x)[\mathsf{Var}\circ r]=Tr(k(x)).$$ Thus the representatives agree pointwise. Well-definedness follows from lemma 23.10. ◻

The identity and composition laws for the source functor action now follow from theorem 23.11; the functor action used in lemma 23.5 and the monadic substitution are therefore compatible.

Syntactic equations at three constructors

The monad laws determine substitution and composition at the three running constructors. The following calculations expose the relevant recursive position in each case.

Ordinary choice.

For $f:A\to TB$, $$\mathsf{or}(t,u)\gg =f=\mathsf{or}(t\gg =f,u\gg =f).$$ The operation is algebraic because both recursive children are response continuations.

Once.

For a smart once node, $$\mathsf{once}(t)\gg =f=\mathsf{once}(t;f),$$ not $\mathsf{once}(t\gg =f)$. The scope body is not a continuation branch.

Local state.

For the source’s smart constructor, $$\mathsf{local}(n,s,t):=\mathsf{local}(n,s,t;\mathsf{Var}),$$ and therefore $$\mathsf{local}(n,s,t)\gg =f=\mathsf{local}(n,s,t;f).$$ The ordinary parameters $n,s$ are stable, the local computation $t$ stays inside the scope, and the continuation becomes $f$. An implementation which changes every field under bind has confused three different parts of the signature.

Equations (23.26)–(23.28) belong to the abstract syntax monad; an operational interpretation requires a separate handler algebra.

Exact comparisons with neighboring abstractions

The words idiom, arrow, scoped operation, and higher-order operation describe different structures. Similar-looking examples are not a translation. We compare them only where a map can be written or a type obstruction can be exhibited.

From the scoped monad to an idiom

Every instance of the scoped syntax monad yields an applicative/idiom structure by the standard monadic translation

Proof of Proposition 23.15 — Monad-induced idiom

Proof. Expand $\mathsf{pure}$ and by (23.29). Identity and homomorphism reduce directly by the unit laws: and

For interchange, put ${\mathsf{ev}}_y(h):=h(y)$. Both sides reduce to the same term:

For composition, factor both sides through the common normal form $$N:=u\gg =\lambda f.v\gg =\lambda g.w\gg =\lambda x.\mathsf{return}(f(g(x))).$$ Application associates to the left. Put Expansion of (23.29), followed by left unit, gives $$P=\begin{array}{c}u\gg =\lambda f.v\gg =\lambda g.\hfill \\ \hfill \mathsf{return}(f\circ g).\end{array}$$ Expanding the final application and reassociating therefore yields On the right, first expand the inner application and then reassociate:  ◻

Equation (23.29) is the exact one-way translation used here. We do not infer a converse from the applicative interface: $\mathsf{pure}$ and do not themselves define an operation of bind’s dependent type. This is a signature boundary, not a nondefinability theorem. Lindley’s comparison of idioms, arrows, and monads is used only as neighboring vocabulary, not as a theorem about our scoped signature [Lin14].

The Kleisli arrow

For the arrow comparison, use the exact Kleisli category of the monad and its cartesian product action; no abstract Arrow law package is imported. Take an arrow from $A$ to $B$ to be a function $A\to TB$, and define

Proof of Proposition 23.16 — Kleisli category and product action

Proof. All equations are pointwise. For the left identity, For the right identity, Ordinary composition is preserved because Associativity is For the first product equation, For the second product equation, define $$N_e:=p(a)\gg =\lambda b.q(b)\gg =\lambda c.\mathsf{return}(c,e).$$ The left side reduces as follows: The right side reduces to the same term: Function extensionality completes each equation. ◻

This construction is one-way. An arbitrary arrow interface does not by itself select a canonical family of carriers $TA$, a return injection $A\to TA$, or the explicit scoped constructors (23.6). No converse reconstruction is claimed.

Scoped operations versus higher-order operations

The scoped signature (23.4) has one intermediate result set $X$ at a scope node. Consequently every owned computation $$m(q):TX(q\in Q_s)$$ returns the same $X$, and the outside continuation has domain exactly $X$: $$k:X\to TA.$$ A higher-order operation has a different interface. Its fork positions may have result sets $B_q$, while the operation itself has an independently specified response set $R$. Its node data therefore have the shape $${\psi }_q:H{B}_q(q\in Q),\kappa :R\to HA.$$ Here $H$ names the later higher-order syntax only for this comparison; it is not identified with $T$.

To isolate the shape question, suppose a sortwise translation $${\tau }_Z:HZ\to TZ$$ is fixed for every set $Z$. This is an explicit assumption, not a translation theorem about the later calculus. Put $$X:=\coprod _{q\in Q}{B}_q,{\hat{\psi }}_q:={\tau }_{B_q}({\psi }_q),\hat{\kappa }(r):={\tau }_A(\kappa (r)).$$ A first failed counterexample points only to the heterogeneous sets $B_q$. That objection is too weak: functorial renaming gives $$T{\mathsf{in}}_q({\hat{\psi }}_q):TX(q\in Q).$$ Thus tags repair heterogeneity. They do not repair the continuation: $\hat{\kappa }$ has domain $R$, while a scoped node over the coproduct carrier needs a continuation with domain $X$.

Proof of Proposition 23.18 — Continuation-adapter criterion

Proof. Given $\rho :X\to R$, precomposition defines (23.33). For $u:Y\to Z$, $$u\circ {\mathrm{\Phi }}_Y(\ell )\stackrel{definition}{=}u\circ \ell \circ \rho \stackrel{definition}{=}{\mathrm{\Phi }}_Z(u\circ \ell ),$$ so (23.34) holds.

Conversely, let $\mathrm{\Phi }$ satisfy the naturality equation and put $\rho :={\mathrm{\Phi }}_R({\mathsf{id}}_R)$. For any set $Y$ and map $\ell :R\to Y$, apply naturality from codomain $R$ to codomain $Y$, with post-map $\ell$ and continuation ${\mathsf{id}}_R$. Then $$\ell \circ \rho \stackrel{definition}{=}\ell \circ {\mathrm{\Phi }}_R({\mathsf{id}}_R)\stackrel{(23.34)}{=}{\mathrm{\Phi }}_Y(\ell \circ {\mathsf{id}}_R)\stackrel{\text{identity law}}{=}{\mathrm{\Phi }}_Y(\ell ).$$ Hence every structural translation is precomposition with the recovered adapter. Recovering an adapter from precomposition returns the original $\rho$, and reconstructing $\mathrm{\Phi }$ from the recovered adapter returns the original family by the displayed calculation. ◻

The criterion gives a genuine counterexample. Take two fork positions with $$B_L=\mathbb{N},B_R=\mathbf{2},R=\varnothing .$$ At the level of the interface (23.31), take $H=\mathsf{Id}$ and ${\tau }_Z=\mathsf{Var}:Z\to TZ$. Choose ${\psi }_L=0$, ${\psi }_R=\mathsf{false}$, and use the unique continuation Here $\varnothing$ is the empty response set, corresponding to the empty type $0$ used for response domains in chapter 22. Thus $\varnothing \to A$ is a singleton function space. The higher-order node is therefore well formed, and all of its computation-valued fields have the assumed translation. The coproduct carrier $X=\mathbb{N}+\mathbf{2}$ makes the fork homogeneous, but no function $X\to \varnothing$ exists. More generally, any common carrier $C$ reached by maps from both inhabited fork-result sets is inhabited, so it cannot admit an adapter $C\to \varnothing$. By proposition 23.18, there is no structural conversion of this node to the scoped shape using only functorial fork translations and a natural continuation conversion.

There are restricted positive bridges. Suppose the sortwise translation $\tau$ above is fixed, a scoped symbol $s$ has $Q_s=Q$, a matching ordinary parameter $p:P_s$ and an operation-specific adapter $\rho :X\to R$ are supplied. Then the translated node is exactly $${\mathsf{Scope}}_s(p;X;\lambda q.T{\mathsf{in}}_q({\tau }_{B_q}({\psi }_q));\hat{\kappa }\circ \rho ).$$ Equation (23.32) translates the fork positions and (23.35) changes the continuation domain. Taking $R=X$ and $\rho ={\mathsf{id}}_X$ is the simplest case. The adapter is additional operation-specific signature data; it is absent from an arbitrary higher-order operation. This conditional node translation proves neither inclusion nor equivalence of the two calculi, and it transfers no elaboration theorem from the separate higher-order system.

Sources and mathematical scope

The syntax (23.5)–(23.6), the explicit-continuation reading, the source bind clause (23.18), and the nondeterminism, exceptions, and local-state signatures come from Piróg, Schrijvers, Wu, and Jaskelioff [PSWJ18]. The algebraicity obstruction in (23.2)– (23.3) is their motivating calculation. This chapter proves the elementwise reindexing, substitution equations, and monad laws locally rather than using a citation as a proof. The reindexing equation in definition 23.4 is the elementwise form of the explicit-substitution quotient in Section 3 of that source.

Plotkin and Power characterize the first-order commutation boundary recalled from chapter 22 [PP03]. Lindley gives the neighboring idiom/arrow terminology [Lin14]; the concrete translations (23.29)–(23.30) are proved directly here.

Operational handlers require an evaluation relation and typing judgment not present in this syntax, so their safety theorems begin from additional data. Likewise, higher-order modular elaboration is a separate calculus rather than a metatheorem of $T$.