ch:scoped-operations: ch:scoped-operations

The body $M^{\prime }$ writes $s_0+1$ and returns $7$. The continuation $k^{\prime }$ is pure and returns $8$. Thus the scope boundary is not observed: The original $k$ raises. On the left of (23.1) that raise occurs after the transaction has committed; on the right it occurs before the transaction closes and therefore triggers rollback. Algebraicity is a universal equation in the continuation. Finding one continuation $k^{\prime }$ for which the two sides agree proves nothing about the failing continuation $k$, which is already a counterexample to the universal law.

Take ordinary operation symbols $\mathcal{O}=\{\mathsf{fail},\mathsf{or}\}$ and one scoped symbol $\mathcal{S}=\{\mathsf{once}\}$. One convenient polynomial presentation is Hence their elementwise formation data are The last constructor is taken modulo the reindexing equation (23.12). The first two polynomial summands give $1+X\times X$, and the scoped polynomial summand gives the unary functor $\mathrm{\Gamma }X\cong X$.

For raise, take one ordinary operation family parameterized by the exception: $P_{\mathsf{raise}}=E$ and $R_{\mathsf{raise}}=0$. Its polynomial summand is therefore $E\times X^0\cong E$.

For catch, take one scoped symbol with $P_{\mathsf{catch}}=1$ and $$Q_{\mathsf{catch}}=1+E.$$ Then $$X^{1+E}\cong X\times X^E,$$ so the distinguished left position stores the protected computation and the $e$-position stores the recovery computation for exception $e$. Every position has type $TX$ for one common intermediate set $X$. In particular, the protected computation and all recovery computations must return the same intermediate result type before the outside continuation is entered.

The canonical representative is $$[TA,m^{\prime },{\mathsf{id}}_{TA}],m^{\prime }(L)=Tk(m(L)),m^{\prime }(R)=Tk(m(R)).$$ Now suppose $k=k^{\prime }\circ h$. Packing the original representative gives Packing the reindexed representative gives exactly $$\mathsf{pack}[Y,\lambda q.Th(m(q)),k^{\prime }](q)\stackrel{(23.13)}{=}T{k}^{\prime }(Th(m(q))).$$ The two packed families agree pointwise at $L$ and $R$.

By the ordinary clause of explicit substitution, There are two $\mathsf{or}$-nodes. The outer node is the original choice; the inner left node came from the replacement computation $f(1)$.

The correct calculation is The original scoped choice tree is unchanged; $f$ is stored as the outside continuation.

Both bad candidates transform the body to $$t[f]\stackrel{(23.17)}{=}\mathsf{or}(\mathsf{or}(\mathsf{Var}(1),\mathsf{Var}(2)),\mathsf{or}(\mathsf{Var}(5),\mathsf{Var}(6))).$$ Those two new inner $\mathsf{or}$-nodes have been moved under $\mathsf{once}$. False algebraicity produces $\mathsf{once}(t[f];\mathsf{Var})$, so it loses $f$ from the outside continuation. The all-fields traversal (23.16) instead produces $\mathsf{once}(t[f];f)$: it transforms the body and also composes after the scope. These two erroneous trees are therefore distinct.

Definition 23.9 gives $$\mathsf{local}(n,s,t;k)[f]\stackrel{(23.21)}{=}\mathsf{local}(n,s,t;\lambda x.k(x)[f]).$$ Writing the first three fields of the displayed result as $(n_f,s_f,t_f)$, constructor injectivity gives $$(n_f,s_f,t_f)=(n,s,t).$$ An implementation which changed an ordinary parameter would violate the first two components; one which descended into the scoped body would violate the third. Neither conclusion depends on an interpretation of local state.

By (23.25) and right identity, For $f:A\to B$ and $g:B\to C$, Left unit is used exactly in the third line, where substitution into the returned variable $\mathsf{Var}(f(a))$ collapses to $\mathsf{Var}(g(f(a)))$.

By the definition of $\mathsf{first}$, The owned computation remains exactly $t_a:TX$. The outside continuation changes from $k_a$ to $$x⟼k_a(x)\gg =\lambda b.\mathsf{return}(b,c),$$ which pairs the final result with the untouched component $c$ only after the scope has closed.

Take a single scoped symbol $\mathsf{transaction}$ with $P_{\mathsf{transaction}}=1$ and $Q_{\mathsf{transaction}}=1$. Its scoped functor is therefore the identity. For $M:TX$ and $k:X\to TA$, write $$\mathsf{transaction}(M;k):={\mathsf{Scope}}_{\mathsf{transaction}}(\ast ;X;\lambda \mathrm{\_}.M;k).$$ Correct substitution gives $$\mathsf{transaction}(M;k)\gg =f\stackrel{(23.20)}{=}\mathsf{transaction}(M;\lambda x.k(x)\gg =f).$$ The body $M$ is unchanged.

The false-algebraicity candidate is $$\mathsf{transaction}(M\gg =(\lambda x.k(x)\gg =f);\mathsf{Var}).$$ It is body-only: it moves the stored continuation and the new bind into the rollback region, then loses them from the outside continuation. Specializing $k=\mathsf{Var}$ gives exactly the failure exhibited by (23.1).

By contrast, the all-fields traversal (23.16) tries to transform both $M:TX$ and the outside continuation. It is ill typed unless $X=A=B$. In that endomorphic homogeneous case it duplicates the post-computation: it moves $f$ into the body and also retains it after the scope. Thus the type failure belongs to the generic all-fields clause, whereas false algebraicity is typed but has the wrong transactional boundary.

For $Q_s=\{1,2\}$, equation (23.12) with $m(1)=m_1$ and $m(2)=m_2$ is exactly $$[X,(m_1,m_2),k\circ h]\stackrel{(23.12)}{=}[Y,(Th(m_1),Th(m_2)),k].$$ Let $f:A\to TB$ and put $k_f(y)=k(y)[f]$. Substitution on the left produces $$[X,(m_1,m_2),k_f\circ h],$$ while substitution on the right produces $$[Y,(Th(m_1),Th(m_2)),k_f].$$ These are related by the same generator (23.12). The two scoped computations remain untouched throughout; only the outside continuation changes.

Write $Q=1+E$, with protected position $\star$ and recovery positions $e:E$. Define the family $$m(\star ):=M,m(e):=H(e).$$ The catch node is $$C:={\mathsf{Scope}}_{\mathsf{catch}}(\ast ;X;m;k).$$ For $f:A\to TB$, $$C\gg =f\stackrel{(23.20)}{=}{\mathsf{Scope}}_{\mathsf{catch}}(\ast ;X;m;\lambda x.k(x)\gg =f).$$ Neither $M$ nor any $H(e)$ changes. A second bind by $g:B\to TC$ gives the calculation The last term is the one-step substitution by the composite continuation. The proof is syntactic; no exception interpretation is used.

The elementwise smart constructor is $$\mathsf{once}(t):=[A,\lambda \mathrm{\_}.t,\mathsf{Var}].$$ Packing gives the canonical body $$\mathsf{pack}[A,\lambda \mathrm{\_}.t,\mathsf{Var}]\stackrel{(23.13)}{=}\lambda \mathrm{\_}.T\mathsf{Var}(t):1\to T(TA).$$ Thus the nested node is $$\mathsf{Scope}(\mathsf{Once}(T\mathsf{Var}(t))),$$ exactly the source’s $\mathsf{fmap}\mathsf{return}$ construction.

After substitution by $f:A\to TB$, the elementwise node is $[A,\lambda \mathrm{\_}.t,f]$. Reindex it along $f:A\to TB$, with final continuation ${\mathsf{id}}_{TB}$, to obtain $$[TB,\lambda \mathrm{\_}.Tf(t),{\mathsf{id}}_{TB}].$$ For a general canonical scope whose body is $u:T(TA)$, the same reindexing uses the function $b_f:TA\to TB$, $b_f(v)=v\gg =f$, and yields body $T{b}_f(u)$. Applying the scoped functor therefore gives $$\mathsf{Scope}(v)\gg =f\stackrel{(23.18)}{=}\mathsf{Scope}(\mathrm{\Gamma }(T{b}_f)(v)),$$ which is (23.18). The first canonicalization uses functorial renaming $T\mathsf{Var}$; the second uses reindexing (23.12) followed by the functor action $T{b}_f$.

Let ${\tau }_Z:HZ\to TZ$ be the assumed sortwise translation. Put $${\hat{\psi }}_L:={\tau }_{\mathbb{N}}({\psi }_L):T\mathbb{N},{\hat{\psi }}_R:={\tau }_{\mathbf{2}}({\psi }_R):T\mathbf{2},$$ and translate the continuation pointwise by $$\hat{\kappa }(r):={\tau }_A(\kappa (r)):TA.$$ With $X:=\mathbb{N}+\mathbf{2}$, functorial renaming gives $$T\mathsf{inl}({\hat{\psi }}_L):TX,T\mathsf{inr}({\hat{\psi }}_R):TX.$$ Thus differing fork-result types alone are not an obstruction.

Suppose first that $\rho :X\to R$ is supplied. For every set $Y$, define $${\mathrm{\Phi }}_Y(\ell ):=\ell \circ \rho (\ell :R\to Y).$$ For $u:Y\to Z$, associativity of composition gives so the family is natural in $Y$.

Conversely, suppose $\mathrm{\Phi }$ is natural, and define $$\rho :={\mathrm{\Phi }}_R({\mathsf{id}}_R):X\to R.$$ For any $\ell :R\to Y$, naturality with post-map $\ell :R\to Y$ gives Thus every natural family is precomposition by the recovered adapter. The two constructions are inverse by the same equations.

Now take $R=\varnothing$. The carrier $X=\mathbb{N}+\mathbf{2}$ is inhabited by $\mathsf{inl}(0)$. If $\rho :X\to \varnothing$ existed, then $\rho (\mathsf{inl}(0))$ would be an element of the empty set, a contradiction. Hence the fork can be homogenized, but its continuation domain cannot be structurally converted to the scoped carrier.

For the restricted positive case, take $R=X$ and $\rho ={\mathsf{id}}_X$. Then $${\mathrm{\Phi }}_Y(\ell )\stackrel{translationdefinition}{=}\ell \circ {\mathsf{id}}_X\stackrel{\text{identity law}}{=}\ell ,$$ so the continuation already has the scoped domain. For a scoped symbol with the two fork positions and a matching parameter $p:P_s$, the complete translated node is $${\mathsf{Scope}}_s(p;X;(T\mathsf{inl}({\hat{\psi }}_L),T\mathsf{inr}({\hat{\psi }}_R));\hat{\kappa }).$$ The response identification, equivalently the adapter $\rho :X\to R$, is additional operation-specific signature data. An arbitrary higher-order signature does not contain it, so this conditional bridge is not an equality or a general inclusion of the two calculi.