Lexical handlers, stack switching, and clue search

This section freezes the three distinct cards used by chapter 34. Identical letters in different cards do not identify their syntactic categories or configuration relations.

Untyped Lexa roots

Lexa configurations and contexts are $$C=⟨M\mid H\mid K\mid E\mid t⟩.$$ Abbreviate the two stored frames by $$\mathcal{F}(E,x,t):=(E,\mathsf{let}x=[]\mathsf{in}t),\mathcal{H}(L,P,L_{\mathrm{e}\mathrm{n}\mathrm{v}}):=\mathsf{hdl}(L,P,L_{\mathrm{e}\mathrm{n}\mathrm{v}},[]).$$ Then $$K::=ϵ\mid K\cdot \mathcal{F}(E,x,t)\mid K\cdot \mathcal{H}(L,P_o,L_{\mathrm{e}\mathrm{n}\mathrm{v}}).$$ The three characteristic roots are: $$\begin{array}{c}⟨M\mid H\mid K\mid E\mid \mathsf{let}x=\mathsf{handle}{P}_b\mathsf{with}{P}_o\mathsf{under}{v}_{\mathrm{e}\mathrm{n}\mathrm{v}}\mathsf{in}t⟩\\ ⟶⟨M\mid H\mid K\cdot \mathcal{F}(E,x,t)\cdot \mathcal{H}(L,P_o,L_{\mathrm{e}\mathrm{n}\mathrm{v}})\mid E_b\mid t_b⟩,\\ ⟨M\mid H\mid K\cdot \mathcal{H}(L,P_o,L_{\mathrm{e}\mathrm{n}\mathrm{v}})\cdot K^{\prime }\mid E\mid \mathsf{let}x=\mathsf{raise}Lv\mathsf{in}t⟩\\ ⟶⟨M\mid H[L_k\mapsto \mathsf{cont}(K_k)]\mid K\mid E_o\mid t_o⟩,\\ ⟨M\mid H\mid K\mid E\mid \mathsf{let}x=\mathsf{resume}{L}_{k}v\mathsf{in}t⟩\\ ⟶⟨M\mid H[L_k\mapsto \mathsf{ns}]\mid K\cdot \mathcal{F}(E,x,t)\cdot K^{\prime }\mid E^{\prime }[x^{\prime }\mapsto E(v)]\mid t^{\prime }⟩.\end{array}$$ In the first root, $L$ is fresh, $M(P_b)=\lambda (x_{\mathrm{e}\mathrm{n}\mathrm{v}},x_{\mathrm{h}\mathrm{d}\mathrm{l}}).t_b$, and $E_b=[x_{\mathrm{e}\mathrm{n}\mathrm{v}}\mapsto L_{\mathrm{e}\mathrm{n}\mathrm{v}},x_{\mathrm{h}\mathrm{d}\mathrm{l}}\mapsto L]$. In the second, $$\begin{array}{c}{K}_k=\mathcal{H}(L,P_o,L_{\mathrm{e}\mathrm{n}\mathrm{v}})\cdot K^{\prime }\cdot \mathcal{F}(E,x,t),\\ M(P_o)=\lambda (x_{\mathrm{e}\mathrm{n}\mathrm{v}},y,k).t_o,E_o=[x_{\mathrm{e}\mathrm{n}\mathrm{v}}\mapsto L_{\mathrm{e}\mathrm{n}\mathrm{v}},y\mapsto E(v),k\mapsto L_k],\end{array}$$ and $L_k$ is fresh. In the third, $H(L_k)=\mathsf{cont}(K^{\prime }\cdot (E^{\prime },\mathsf{let}{x}^{\prime }=[]\mathsf{in}{t}^{\prime }))$. The raise factorization is by identity $L$; the resume premise requires a continuation cell, not $\mathsf{ns}$.

Salt interface and selected translation

Salt has configurations $⟨M\mid H\mid R⟩$, words $w::=L\mid P\mid i\mid \mathsf{ns}$, and the general instruction set in section 34.3. Its selected translation is The ordinary handle trampoline allocates a stack and pushes $P_o::L_{\mathrm{e}\mathrm{n}\mathrm{v}}::A::{\ell }_{\mathrm{e}\mathrm{x}\mathrm{c}\mathrm{h}}$. Raise exchanges the header’s saved pointer with the current stack top and allocates a one-cell resumption that points to the exchanger. Resume first writes $\mathsf{ns}$ to that cell, exchanges stack pointers, and returns on the reinstated stack.

SL/TL clue interface

The 2025 joint typing-and-translation judgment is $$\mathrm{\Theta }\mid \mathrm{\Delta }\mid \mathrm{\Sigma }\mid \mathrm{\Gamma }⊢t:\tau ⇝\underset{―}{t}.$$ A TL clue and call-site metadata are $$C=⟨q,F⟩,q::=\hat{i}\mid \mathring{i}\mid \mathrm{\infty },\mathcal{H}=T_0;T;\overline{\ell }:\overline{F}.$$ When search crosses a call frame it applies ${\mathsf{hopper}}_{\mathcal{H}}$. The label-parameter case is $${\ell }_i:F\mapsto \hat{j}⟹{\mathsf{hopper}}_{\mathcal{H}}(⟨\hat{i},F⟩)=⟨\hat{j},F⟩.$$ Capability and capture cases inspect $T$ and $T_0$, respectively. Their premises require a unique label with the requested effect name, or a unique capability index to continue following. Thus the hopper is partial on arbitrary triples but defined on metadata produced by the selected well-typed translation.

Generalised-continuation card

The ${\lambda }^{†}$ source has computation types $A!E$ and handler types $C{\Rightarrow }_{\delta }D$, where $\delta \in \{\mathsf{deep},†\}$. Its higher-order CPS target is the untyped two-level calculus with generalised continuation frames $$⟨\theta ,⟨{\chi }_{\mathrm{r}\mathrm{e}\mathrm{t}},{\chi }_{\mathrm{o}\mathrm{p}\mathrm{s}}⟩⟩::\kappa .$$ The selected translation roots are Deep $\mathsf{res}$ retains the handling frame when captured pure frames are prepended. Shallow ${\mathsf{res}}^{†}$ restores the captured frame stack without reinstalling the capturing handler. Parameterised handlers extend a frame with the current parameter and translate locally to ordinary deep handlers; this is a fourth card, not a silent identification with either resumption root.