Chapter 149Optional

Categorical Semantics of Scoped Operations

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

Theorem 23.11 proved that the scoped syntax $T A = μ X . (A + Σ X + Γ (T X))$ of definition 23.2 carries a monad structure, by displaying the substitution operation and checking its three laws on each constructor. The proof is a computation with the clauses of (23.17), and it says nothing about where the structure comes from. Three questions are left open by it. The nesting $T (T A)$ in the scope constructor is not the shape of an algebra for an endofunctor, so $T$ is not visibly a free monad on anything. Interpreting a scoped term needs a carrier for each depth of nesting (example 23.8 used lists of lists), and the elementwise account gives no reason for that. And the monad laws were verified rather than derived, so a second construction of the same monad could not be recognized as the same.

This chapter answers all three at once. The nesting is replaced by two adjoint shift functors on indexed families; the scoped syntax becomes an ordinary free monad for an ordinary endofunctor on the indexed category; and the two presentations are compared by a pair of maps proved mutually inverse. Nothing about chapter 23 changes: the elementwise monad is the object of study, and the categorical monad is a second description of it.

The signature and the elementwise monad, restated

Convention 149.1 — The frozen signature ¶

Fix the scoped signature $(Σ, Γ)$ of definition 23.1: two endofunctors on $Set$ , presented elementwise by (23.4) as $Σ X = \underset{o}{∐} P_{o} \times X^{R_{o}}$ and $Γ X = \underset{s}{∐} P_{s} \times X^{Q_{s}}$ . Write $E$ for the scoped syntax monad $T$ of definition 23.2, with constructors $Var$ , $Op$ , $Scope$ as in (23.6) and with unit and multiplication as in (23.23). The hypothesis of definition 23.2 on the initial chain remains in force, and the base category is $Set$ throughout; where a general $C$ would do, the argument is the same and is not stated more generally.

Referenced from 4 locations

Categorical Semantics of Scoped Operations

The letter $E$ is used for the elementwise monad so that the comparison in section 149.4 has two names to compare.

Indexed families and the two shifts

Definition 149.2 — The indexed category ¶

Let $| N |$ be the discrete category on the natural numbers and let ${Set}^{| N |}$ be the functor category: an object is a family $A = (A_{n})_{n \in N}$ of sets and an arrow $A ⟶ B$ is a family $(f_{n} : A_{n} \to B_{n})$ , with no condition relating different indices. Coproducts are computed indexwise, $(A + B)_{n} = A_{n} + B_{n}$ , and an endofunctor $Σ$ on $Set$ lifts indexwise by $(Σ A)_{n} : = Σ (A_{n})$ .

Referenced from 3 locations

Categorical Semantics of Scoped Operations

The index $n$ will be the number of scopes enclosing a subterm. Two operations move a family along that count.

Definition 149.3 — Shift left and shift right ¶

On ${Set}^{| N |}$ put $(◃ A)_{i} : = A_{i + 1}, (▹ A)_{0} : = \emptyset, (▹ A)_{i + 1} : = A_{i},$ with the evident action on arrows.

Referenced from 3 locations

Categorical Semantics of Scoped Operations

Lemma 149.4 ¶

$▹$ is left adjoint to $◃$ . Consequently arrows $A ⟶ ◃ B$ correspond bijectively and naturally to arrows $▹ A ⟶ B$ .

Referenced from 3 locations

Categorical Semantics of Scoped Operations

Proof of Lemma 149.4

Proof. An arrow $▹ A ⟶ B$ is a family $(g_{i} : (▹ A)_{i} \to B_{i})$ . At $i = 0$ the domain is $\emptyset$ , so $g_{0}$ is the unique empty map and carries no data; at $i + 1$ the domain is $A_{i}$ , so the remaining data is a family $(g_{i + 1} : A_{i} \to B_{i + 1})$ , which is exactly an arrow $A ⟶ ◃ B$ . The two assignments are mutually inverse by construction, and both are natural in $A$ and $B$ because they only reindex the components. The two equations of (142.5) are these reindexings. ◻

Definition 149.5 — Scoped algebra ¶

A scoped algebra for $(Σ, Γ)$ is a quadruple $⟨ A, a : Σ A ⟶ A, d : Γ ◃ A ⟶ A, p : A ⟶ ◃ A ⟩$ in ${Set}^{| N |}$ . The arrow $d$ is the demotion interpreting a scope creator and $p$ is the promotion performed on entering a scope.

Referenced from 5 locations

Categorical Semantics of Scoped Operations

Proposition 149.6 — Scoped algebras are ordinary algebras ¶

Scoped algebras for $(Σ, Γ)$ are exactly the algebras for the endofunctor $Σ + Γ ◃ + ▹$ on ${Set}^{| N |}$ , and the two notions of morphism agree.

Referenced from 4 locations

Categorical Semantics of Scoped Operations

Proof of Proposition 149.6 — Scoped algebras are ordinary algebras

Proof. By lemma 149.4 the promotion arrows $p : A ⟶ ◃ A$ correspond bijectively and naturally to arrows $▹ A ⟶ A$ . An algebra for a coproduct of endofunctors is a triple of arrows out of the three summands, so the data $(a, d, p)$ is exactly one arrow $(Σ + Γ ◃ + ▹) A ⟶ A$ . A homomorphism condition for the coproduct algebra is the conjunction of the three componentwise conditions, and the third of these is transported by the bijection because the bijection is natural. ◻

Proposition 149.6 is the whole gain of the indexed category: the nesting $T (T A)$ of (23.5), which is not the shape $A + F X$ of an algebra, has been replaced by an ordinary signature, at the cost of carrying one carrier per scope depth.

Example 149.7 — Nondeterminism with once ¶

Take $Σ X = X \times X + 1$ with injections $or$ and $fail$ , and $Γ X = X$ for the scoped operation $once$ , as in (23.7). For a set $X$ put $A_{n} : = {List}^{n + 1} X$ , the $(n + 1)$ -fold application of the list functor. Interpret $a_{n} (or (x, x^{'})) : = x + + x^{'}, a_{n} (fail) : = [], p_{n} (x) : = [x],$ and let $d_{n}$ select the first element of a list of lists, with $d_{n} ([]) : = []$ . Every component is a function $A_{n} \to A_{n}$ , $A_{n} \to A_{n + 1}$ or $A_{n + 1} \to A_{n}$ of the right type, so this is a scoped algebra. The list-of-lists carrier that example 23.8 produced by hand is here forced: the promotion $p$ must land in $A_{n + 1}$ , and $List$ applied once more is the smallest such choice for this interpretation.

Referenced from 6 locations

Categorical Semantics of Scoped Operations

The free monad and the represented monad

Definition 149.8 — The free scoped monad ¶

Assume the forgetful functor $U : (Σ + Γ ◃ + ▹) - Alg \to {Set}^{| N |}$ has a left adjoint $F$ ; this holds under the initial-chain hypothesis of convention 149.1. Put $M : = U F = (Σ + Γ ◃ + ▹)^{*} : {Set}^{| N |} \to {Set}^{| N |},$ the free monad on that endofunctor, with structure map $in = [η, c_{Σ}, c_{Γ}, c_{▹}]$ .

Referenced from 2 locations

Categorical Semantics of Scoped Operations

Lemma 149.9 — Reading the free monad indexwise ¶

For every family $A$ , $\begin{aligned} (M A)_{0} & ≅ A_{0} + Σ (M A)_{0} + Γ (M A)_{1}, \\ (M A)_{n + 1} & ≅ A_{n + 1} + Σ (M A)_{n + 1} + Γ (M A)_{n + 2} + (M A)_{n} . \end{aligned}$

Referenced from 8 locations

Categorical Semantics of Scoped Operations

Proof of Lemma 149.9 — Reading the free monad indexwise

Proof. By Lambek’s lemma the structure map of the initial algebra is an isomorphism, so $M A ≅ A + Σ M A + Γ ◃ M A + ▹ M A$ . Evaluate at $n$ : $(Γ ◃ M A)_{n} = Γ ((M A)_{n + 1})$ by definition 149.3 and the indexwise lifting, and $(▹ M A)_{0} = \emptyset$ while $(▹ M A)_{n + 1} = (M A)_{n}$ . A coproduct with $\emptyset$ is the other summand. ◻

The four summands read as four constructors. A variable at index $n$ ; an ordinary operation whose arguments sit under the same $n$ scopes; a scope creator, an opening bracket, whose arguments sit under $n + 1$ scopes; and a closing bracket whose argument is the continuation, outside the innermost scope, hence under $n - 1$ . The absence of the fourth summand at index $0$ is the statement that every closing bracket matches an opening one.

Theorem 149.10 — The projection adjunction ¶

The functor $⇂ : {Set}^{| N |} \to Set$ with $⇂ A : = A_{0}$ has a left adjoint $↾$ given by $(↾ X)_{0} : = X$ and $(↾ X)_{n + 1} : = \emptyset$ . Consequently $⇂ M ↾$ is a monad on $Set$ .

Referenced from 4 locations

Categorical Semantics of Scoped Operations

Proof of Theorem 149.10 — The projection adjunction

Proof. An arrow $↾ X ⟶ A$ is a family whose component at $0$ is a function $X \to A_{0}$ and whose components at $n + 1$ are the unique maps out of $\emptyset$ ; so it is exactly a function $X \to ⇂ A$ , naturally in $X$ and $A$ . This is the hom-set bijection of definition 142.17, and the two equations (142.5) are again reindexings. Composing $↾ ⊣ ⇂$ with $F ⊣ U$ by lemma 142.37 gives $F ↾ ⊣ ⇂ U$ , whose induced monad on $Set$ has underlying functor $⇂ U F ↾ = ⇂ M ↾$ . ◻

Sandwiching in this way is what removes variables from inside scopes: since $(↾ X)_{n + 1} = \emptyset$ , lemma 149.9 leaves no variable summand at a positive index, which matches the elementwise fact that substitution acts only on the outermost continuation ((23.17)).

The comparison

Two monads on $Set$ are now in play: the elementwise $E$ of convention 149.1 and the represented $⇂ M ↾$ of theorem 149.10. The comparison is built from a distributive law that puts $M$ -structure inside brackets.

Definition 149.11 — Bracketing ¶

Let $λ : M ◃ ⟶ ◃ M$ be the unique arrow induced by the algebra structure on $◃ M A$ whose four components are $\begin{aligned} λ_{var} & : = ◃ η : ◃ A ⟶ ◃ M A, \\ λ_{Σ} & : = ◃ c : Σ ◃ M A = ◃ Σ M A ⟶ ◃ M A, \\ λ_{◃} & : = ◃ c : Γ ◃ ◃ M A = ◃ Γ ◃ M A ⟶ ◃ M A, \\ λ_{▹} & : = ◃ c \circ ε : ▹ ◃ M A ⟶ M A = ◃ ▹ M A ⟶ ◃ M A, \end{aligned}$ with $ε$ the counit of $▹ ⊣ ◃$ . The bracketing of $M$ is $M = M ◃ ▹ \overset{λ}{\to} ◃ M ▹$ .

Referenced from 3 locations

Categorical Semantics of Scoped Operations

The equalities $Σ ◃ = ◃ Σ$ and $Γ ◃ = ◃ Γ$ used above hold because $Σ$ and $Γ$ act indexwise and $◃$ only renumbers indices.

Theorem 149.12 — The two monads agree ¶

The monads $E$ and $⇂ M ↾$ are isomorphic in the category of monads on $Set$ and monad morphisms.

Referenced from 7 locations

Categorical Semantics of Scoped Operations

Proof of Theorem 149.12 — The two monads agree

Proof. Both directions are defined by initiality, and each is then checked to be a monad morphism; the two composites are identities by a second appeal to initiality.

The arrow $i : E ⟶ ⇂ M ↾$ . By definition 23.2, $E$ is the initial algebra of $X \mapsto Id + Σ X + Γ X X$ in the sense that $E A ≅ A + Σ (E A) + Γ (E (E A))$ , so an arrow out of $E$ is determined by three components. Take $\begin{aligned} i_{var} & : = (Id \overset{η}{\to} ⇂ ↾ \overset{⇂ η}{\to} ⇂ M ↾), \\ i_{Σ} & : = (Σ ⇂ M ↾ = ⇂ Σ M ↾ \overset{⇂ c}{\to} ⇂ M ↾), \\ i_{Γ} & : = (Γ ⇂ M ↾ ⇂ M ↾ \overset{Γ ⇂ M ε}{\to} Γ ⇂ M M ↾ = Γ ⇂ M ◃ ▹ M ↾ \overset{Γ ⇂ λ}{\to} Γ ⇂ ◃ M ▹ M ↾ \\ = ⇂ Γ ◃ M ▹ M ↾ \overset{⇂ c c}{\to} ⇂ M M ↾ \overset{⇂ μ}{\to} ⇂ M ↾), \end{aligned}$ and let $i$ be the induced arrow. The middle composite is where the bracketing is used: a scoped operation of $E$ owns a term whose own variables are terms, and the bracketing converts that nesting into an opening and a closing bracket in $M$ .

The arrow $k$ and the inverse. For an endofunctor $G$ on $Set$ define $G^{+} : Set \to {Set}^{| N |}$ by $(G^{+} A)_{n} : = G^{n + 1} A$ . Using $M A = μ X . (A + Σ X + Γ ◃ X + ▹ X)$ , define $k : M ↾ A ⟶ E^{+} A$ by initiality from the four components: the variable component is $η : A \to E A = (E^{+} A)_{0}$ ; the $Σ$ and $Γ$ components are the corresponding constructors of $E$ applied indexwise; and the $▹$ component at index $n + 1$ is $(▹ E^{+} A)_{n + 1} = (E^{+} A)_{n} = E^{n + 1} A \overset{η}{\to} E E^{n + 1} A = (E^{+} A)_{n + 1}$ . Put $i^{- 1} : = ⇂ k : ⇂ M ↾ A \to ⇂ E^{+} A = (E^{+} A)_{0} = E A$ .

Mutually inverse. Both $i^{- 1} \circ i$ and the identity are algebra morphisms out of the initial algebra defining $E$ , so they are equal; both $i \circ i^{- 1}$ and the identity are algebra morphisms out of the initial algebra defining $M ↾$ after projecting with $⇂$ , so they are equal.

Monad morphism. Compatibility with the units is the equation $i \circ η^{E} = η^{⇂ M ↾}$ , which is the variable component $i_{var}$ by construction. Compatibility with the multiplications, $i \circ μ^{E} = μ^{⇂ M ↾} \circ i i$ , is proved by initiality: both sides are algebra morphisms from the initial algebra presenting $E E$ , and they agree on each of the three components, the $Γ$ component by naturality of $λ$ and the two monad laws of $M$ . ◻

Theorem 149.12 is Theorem 5.1 of Piróg, Schrijvers, Wu and Jaskelioff, Syntax and semantics for operations with scopes, LICS 2018, physical page 6; definition 149.5 is their Definition 4.1 and theorem 149.10 their Theorem 4.3, both on physical page 5. The proof above follows their sketch and supplies the initiality arguments they leave implicit.

Example 149.13 — The transaction term through the isomorphism ¶

Exercise 23.1 exhibited the term whose two readings differ, and (23.2) fixed the intended one. Take the term $once (or (Var 1, Var 5)) ≫ = λ x . or (Var x, Var (x + 1)) .$ Under $i$ its image in $⇂ M ↾$ is the term whose root is the opening bracket for $once$ , whose two children are $or$ -nodes at index $1$ , and whose closing brackets return the continuation to index $0$ . Interpreting in the scoped algebra of example 149.7, the $or$ nodes at index $1$ produce $[[1], [2]]$ and $[[5], [6]]$ , the demotion $d$ selects the first, and the result is $[1, 2]$ : the same answer that (23.2) required, now obtained from the algebra rather than by hand.

Referenced from 3 locations

Categorical Semantics of Scoped Operations

Exercise 149.1 ¶

★☆☆ Compute the unit and counit of $▹ ⊣ ◃$ componentwise, and check the two triangle identities (142.6) at indices $0$ and $n + 1$ separately.

Referenced from 2 locations

Categorical Semantics of Scoped Operations

Exercise 149.2 ¶

★★☆ Prove from lemma 149.9 that for $A = ↾ X$ every element of $(M A)_{n}$ with $n > 0$ contains at least one closing-bracket constructor on the path to each variable. Which summand of the lemma is empty, and why?

Referenced from 2 locations

Categorical Semantics of Scoped Operations

Exercise 149.3 ¶

★★☆ Take $Σ X : = S$ and $Γ X : = X \times X^{S}$ for a set $S$ of exceptions, so that the second component of $Γ$ is the handler. Exhibit a scoped algebra with carrier $A_{n} : = H^{n + 1} X$ for a suitable $H$ , and identify the demotion morphism as the handler application.

Referenced from 2 locations

Categorical Semantics of Scoped Operations

What the representation does not cover

Remark 149.14 — Higher-order signatures ¶

Definition 149.5 takes $Γ$ to be an endofunctor applied to $◃ A$ , so a scope creator owns a fixed family of scoped computations indexed by a set $Q_{s}$ and nothing else. A signature in which the scoped argument is itself a function of the enclosing computation — so that the operation inspects or transforms the term it scopes over — is not of this shape, and theorem 149.12 says nothing about it. Such signatures are treated by an intrinsically typed elaboration with its own lawfulness equations; that treatment is a different construction with a different invariant, and no theorem of this chapter transfers to it.

Referenced from 3 locations

Categorical Semantics of Scoped Operations

Remark 149.15 — This is not a handler-correctness theorem ¶

Theorem 149.12 compares two monads. It does not say that a particular handler implementation is correct, that handlers compose in a given order, or that a scoped operation commutes with any effect. It also does not make chapter 23 depend on category theory: every statement of that chapter was proved there from the elementwise clauses, and the isomorphism is a second description added afterwards.

Referenced from 2 locations

Categorical Semantics of Scoped Operations

Suggested first pass.

Begin with exercise 149.4 and exercise 149.5, then complete exercise 149.7.

Exercise 149.4 ¶

★★☆ Write out the isomorphism of lemma 149.9 at $n = 0, 1, 2$ for the signature of example 149.7, and count the elements of $(M ↾ X)_{1}$ for $X$ a two-element set and terms of depth at most two.

Referenced from 3 locations

Categorical Semantics of Scoped Operations

Exercise 149.5 ¶

★★★ Verify that $λ$ of definition 149.11 is a distributive law of the monad $M$ over the endofunctor $◃$ : check the two equations $λ \circ η ◃ = ◃ η$ and $λ \circ μ ◃ = ◃ μ \circ λ M \circ M λ$ on each of the four constructors of lemma 149.9.

Referenced from 3 locations

Categorical Semantics of Scoped Operations

Exercise 149.6 ¶

★★☆ Give a signature $(Σ, Γ)$ and a family $A$ for which the promotion $p$ of definition 149.5 cannot be chosen to be a family of bijections, and explain what that says about recovering the enclosing computation after leaving a scope.

Referenced from 2 locations

Categorical Semantics of Scoped Operations

Exercise 149.7 ¶

★★★ Practical project.scoped-monad-comparison Implement both presentations and check the isomorphism on named inputs. The program represents elementwise terms of $E$ over the signature of example 149.7 as trees with the three constructors of (23.6), and represents indexed terms of $M ↾$ as trees with the four constructors of lemma 149.9, each node carrying its index. It implements $i$ and $i^{- 1}$ of theorem 149.12 and the scoped-algebra interpreter of example 149.7.

Invariant. Every indexed term is well indexed: a variable occurs only at index $0$ , an opening bracket at index $n$ has children at index $n + 1$ , a closing bracket at index $n + 1$ has its child at index $n$ , and no closing bracket occurs at index $0$ . The program checks this invariant after every construction and after every step of $i$ and $i^{- 1}$ , and aborts naming the offending node rather than continuing.

Concrete result. For each input term the program prints the image under $i$ , the image of that under $i^{- 1}$ , and either round trip: equal or round trip: differs at followed by the first differing subterm. It also prints the value computed by the scoped-algebra interpreter on both representations.

Acceptance test. Run it on the term of example 149.13. The round trip must print equal; the interpreter must print $[1, 2]$ on both representations; and the printed indexed term must contain exactly one opening bracket at index $0$ and two closing brackets at index $1$ . Run it on the term of exercise 23.1 that exposed the obstruction: the two representations must agree, and the printed value must be the one (23.2) requires and not the one (23.3) would give. A run in which the closing bracket is emitted at index $0$ has implemented $▹$ without its empty component, which is the defect this test detects.

Referenced from 3 locations

Categorical Semantics of Scoped Operations

Sources. Definition 149.2 through theorem 149.12 follow M. Piróg, T. Schrijvers, N. Wu and M. Jaskelioff, Syntax and semantics for operations with scopes, LICS 2018 [PSWJ18]: the indexed category and the two shifts on physical page 5, the definition of scoped algebra as their Definition 4.1 and the reformulation of proposition 149.6 on the same page, the projection adjunction as their Theorem 4.3 and the indexwise reading of lemma 149.9 on physical pages 5–6, the bracketing distributive law and the comparison morphisms on physical page 6, and the monad isomorphism as their Theorem 5.1 on physical page 6. The elementwise construction that this chapter compares against is chapter 23, following Wu, Schrijvers and Hinze [WSH14]. The structured handler-based semantics with its own theorems, and the operational calculus with a type-safety statement, are Yang et al. [Y^+22] and Bosman et al. [BvdBTS24]; neither is used above. The intrinsically typed elaboration mentioned in remark 149.14 is the subject of the following chapter of the effects route and is not imported here.