Higher-order signatures and modular elaboration

An ordinary signature $\mathrm{\Delta }$ consists of operations ${\mathsf{Op}}_{\mathrm{\Delta }}$ and response sets ${\mathsf{Ret}}_{\mathrm{\Delta }}(o)$. Its disjoint sum is $${\mathsf{Op}}_{{\mathrm{\Delta }}_1{\oplus }_{\mathsf{sig}}{\mathrm{\Delta }}_2}={\mathsf{Op}}_{{\mathrm{\Delta }}_1}+{\mathsf{Op}}_{{\mathrm{\Delta }}_2},{\mathsf{Ret}}_{{\mathrm{\Delta }}_1{\oplus }_{\mathsf{sig}}{\mathrm{\Delta }}_2}({\iota }_{i}o)={\mathsf{Ret}}_{{\mathrm{\Delta }}_i}(o).$$ A higher-order signature $H$ consists of $${\mathsf{Op}}_H^{\mathsf{H}},{\mathsf{Fork}}_H(o),{\mathsf{Ret}}_H^{\mathsf{H}}(o).$$ Here ${\mathsf{Fork}}_H(o)$ is itself an ordinary signature and describes the nested computations owned by $o$. The sum $H_1⊞H_2$ is the disjoint sum of operation tags, with fork and return families selected by cases on the tag.

For $A:\mathbf{Set}$, hefty trees have constructors where $$\psi :\prod _{s:{\mathsf{Op}}_{{\mathsf{Fork}}_H(o)}}{\mathsf{Hefty}}_H({\mathsf{Ret}}_{{\mathsf{Fork}}_H(o)}(s)),k:{\mathsf{Ret}}_H^{\mathsf{H}}(o)⟶{\mathsf{Hefty}}_H(A).$$ The source bind traverses only the ordinary continuation: Traversing $\psi$ would push the continuation into operation-owned subcomputations and is generally ill typed.

For a family $G:\mathbf{Set}⟶\mathbf{Set}$, a hefty algebra has components Given $g_X:X⟶G(X)$ at every $X$, its catamorphism is For $G(X)={\mathsf{Free}}_{\mathrm{\Delta }}(X)$ and $g=\mathsf{pure}$, an algebra $E$ is an elaboration and the catamorphism is ${\mathsf{elaborate}}_E$. Component composition is operation-tag dispatch:

The higher-order catch operation at code $t$ has $${\mathsf{Fork}}_{\mathsf{Catch}}(\mathsf{catch}(t))=(\mathbf{2},\lambda b.\mathsf{Val}(t)),{\mathsf{Ret}}_{\mathsf{Catch}}^{\mathsf{H}}(\mathsf{catch}(t))=\mathsf{Val}(t).$$ For a throw insertion witness $w$, write $h={\mathsf{runThrow}}_w$. Its equations and the residual-operation reinjection are The catch component is $$E_{\mathsf{catch}}(\mathsf{catch}(t),\hat{\psi },\hat{k})={\mathsf{mask}}_w(h(\hat{\psi }(\mathsf{tt})))\gg =\mathsf{maybe}(\hat{k},\hat{\psi }(\mathsf{ff})\gg =\hat{k}).$$ The state component used by the chapter discards the final state: