Chapter 150Optional

Categorical Semantics of Coeffects

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

Section 53.5 interpreted three coeffect calculi in $Set$ , one instance at a time: liveness by an option-like family, bounded reuse by a family of tuples, causal dataflow by a family of finite histories. Each verification checked the same three things by hand — that a variable can be read, that two contexts can be merged when a function is built, and that one context can be split when a function is applied — and each checked them against a different concrete carrier.

The repetition is not the problem. The problem is that the three verifications do not compose. Nothing in them says which equations the carrier must satisfy, so a fourth instance has no specification to meet, and the soundness argument cannot be run against an unknown model. What is missing is the structure that transports a contextual requirement through substitution and composition: one operation for sequencing, one for merging, one for splitting, and the laws they obey.

This chapter states that structure, interprets the flat calculus in it, proves the soundness theorem under exactly those laws, and recovers the three concrete models as instances. It proves no theorem about the structural calculus’s operational behavior and no theorem about quantitative or graded-modal type theory; section 150.6 says where each boundary falls.

The two calculi, restated

Convention 150.1 — The frozen cards ¶

Two systems of chapter 53 are used, and only these.

The flat calculus, whose judgment is $Γ @_{f} r ⊢ e : τ$ with one scalar $r$ for the whole context, and whose rules are F-Var, F-Const, F-Abs and F-App. Its scalars carry a sequential composition $⊛$ with unit $use$ , a sharing operation $\oplus_{c}$ , and a meet $\land_{c}$ , together with the order used by subcoeffecting.
The structural calculus, whose judgment is $Γ @_{s} \vec{r} ⊢ e : τ$ with one scalar per variable, and whose rules are S-Abs and S-App.

The operational hypotheses of the two cards are kept separate throughout: theorem 53.2 is a statement about call-by-value reduction with a pure-value argument, theorem 53.5 about call-by-name, and theorem 53.7 about the structural system. Nothing below transports one to another.

Referenced from 4 locations

Categorical Semantics of Coeffects

Indexed comonads

Read a judgment $Γ @_{f} r ⊢ e : τ$ as a morphism whose source is not $[[Γ]]$ but a context decorated by $r$ : $[[Γ @_{f} r ⊢ e : τ]] : C^{r} [[Γ]] ⟶ [[τ]] .$ The family $C^{r}$ is not assumed to be a functor for each $r$ ; the functor action is derived in lemma 150.3. What is assumed is a way to compose two such morphisms, and that assumption determines the definition.

Definition 150.2 — Indexed comonad ¶

Let $(S, ⊛, use)$ be a monoid. An indexed comonad over a category $C$ consists of an object mapping $C^{r} : ob (C) \to ob (C)$ for each $r \in S$ , together with

a family $ε_{A} : C^{use} A ⟶ A$ , the counit, natural in $A$ ;
for each $r, s \in S$ an operation $(-)_{r, s}^{†}$ sending a morphism $f : C^{r} A ⟶ B$ to a morphism $f_{r, s}^{†} : C^{r ⊛ s} A ⟶ C^{s} B$ , natural in $A$ and $B$ ,

such that for all $f : C^{r} τ_{1} ⟶ τ_{2}$ and $g : C^{s} τ_{2} ⟶ τ_{3}$ , $ε \circ f_{r, use}^{†} = f, (ε)_{use, r}^{†} = {id}_{}, (g \circ f_{r, s}^{†})_{r ⊛ s, t}^{†} = g_{s, t}^{†} \circ f_{r, s ⊛ t}^{†} .$

Referenced from 4 locations

Categorical Semantics of Coeffects

Lemma 150.3 — Composition and functor action ¶

Let $C$ be an indexed comonad. Define $g \hat{\circ} f : = g \circ f_{r, s}^{†} : C^{r ⊛ s} τ_{1} ⟶ τ_{3}$ for $f : C^{r} τ_{1} ⟶ τ_{2}$ and $g : C^{s} τ_{2} ⟶ τ_{3}$ , and put $C^{r} (h) : = (h \circ ε)_{use, r}^{†}$ for $h : A ⟶ B$ . Then $\hat{\circ}$ is associative with $ε$ as a two-sided unit, and each $C^{r}$ is a functor.

Referenced from 4 locations

Categorical Semantics of Coeffects

Proof of Lemma 150.3 — Composition and functor action

Proof. Units. For $f : C^{r} τ_{1} ⟶ τ_{2}$ , $ε \hat{\circ} f = ε \circ f_{r, use}^{†} = f$ by the first law, and $f \hat{\circ} ε = f \circ (ε)_{use, r}^{†} = f$ by the second. The index arithmetic matches because $use$ is the unit of $⊛$ .

Associativity. For $f, g$ as displayed and $h : C^{t} τ_{3} ⟶ τ_{4}$ , $h \hat{\circ} (g \hat{\circ} f) \overset{d e f .}{=} h \circ (g \circ f_{r, s}^{†})_{r ⊛ s, t}^{†} \overset{(150.1)}{=} h \circ g_{s, t}^{†} \circ f_{r, s ⊛ t}^{†} \overset{d e f .}{=} (h \hat{\circ} g) \hat{\circ} f .$

Functoriality. $C^{r} ({id}_{A}) = (ε)_{use, r}^{†} = {id}_{}$ by the second law. For $h : A ⟶ B$ and $h^{'} : B ⟶ A^{'}$ , the third law with $r = s = use$ and $t = r$ gives $C^{r} (h^{'}) \circ C^{r} (h) = (h^{'} \circ ε \circ (h \circ ε)_{use, use}^{†})_{use, r}^{†} \overset{f i r s t l a w}{=} (h^{'} \circ h \circ ε)_{use, r}^{†} \overset{d e f .}{=} C^{r} (h^{'} \circ h),$ the index computation using $use ⊛ use = use$ . ◻

Example 150.4 — Comonads are the trivial case ¶

Take $S$ the one-element monoid. Then $ε$ and $(-)^{†}$ are the counit and coextension of an ordinary comonad, and (150.1) are its three laws. So every comonad is an indexed comonad; the converse fails, and the next example says why.

Referenced from 2 locations

Categorical Semantics of Coeffects

Example 150.5 — Liveness ¶

Take $S = {D, L}$ with $⊛$ the meet of the order $D < L$ and unit $L$ . Put $C^{L} A : = A$ and $C^{D} A : = 1$ , and define $ε x : = x, f_{D, D}^{†} x : = ⋆, f_{D, L}^{†} x : = f ⋆, f_{L, D}^{†} x : = ⋆, f_{L, L}^{†} x : = f x .$ This is an indexed comonad. It is not obtained from a comonad: the only candidate underlying functor is $A \mapsto A + 1$ , whose counit $A + 1 ⟶ A$ is undefined on the right injection, and the indexed counit escapes that by being required only at $C^{L} A = A$ . The clause $f_{D, L}^{†}$ also changes the shape of the context, from $1$ to $B$ , which the shape preservation of an ordinary comonad forbids.

Referenced from 8 locations

Categorical Semantics of Coeffects

Merging and splitting

Sequencing is not enough. Building a function merges the caller’s context with the argument’s; applying one splits a single context into the two the premises need. Each is an extra family of morphisms, and each carries its own index arithmetic.

Definition 150.6 — Indexed lax and colax monoidal structure ¶

Let $C$ have binary products and let $C$ be an indexed comonad whose index set also carries $\land_{c}$ and $\oplus_{c}$ . An indexed lax monoidal structure is a family $m_{r, s} : C^{r} A \times C^{s} B ⟶ C^{r \land_{c} s} (A \times B),$ natural in $A$ and $B$ ; an indexed colax monoidal structure is a family $n_{r, s} : C^{r \oplus_{c} s} (A \times B) ⟶ C^{r} A \times C^{s} B,$ natural in $A$ and $B$ . Both are required to be associative: the two ways of merging, respectively splitting, three factors agree.

Referenced from 11 locations

Categorical Semantics of Coeffects

The two index operations are not interchangeable, and the reason is directional. Merging may lose part of a context, so the result is indexed by the greatest lower bound $r \land_{c} s$ , which is whatever both sides still guarantee. Splitting must supply both halves, so the input must already provide at least $r$ and at least $s$ , and the index is the least upper bound $r \oplus_{c} s$ .

Example 150.7 — Liveness continued ¶

With the liveness algebra of example 150.5, $\begin{aligned} m_{L, L} (x, y) & : = (x, y), & m_{r, s} (x, y) & : = ⋆ otherwise, \\ n_{D, D} (⋆) & : = (⋆, ⋆), & n_{D, L} (x, y) & : = (⋆, y), \\ n_{L, D} (x, y) & : = (x, ⋆), & n_{L, L} (x, y) & : = (x, y) . \end{aligned}$ Each clause has the type required by definition 150.6. For instance $n_{D, L}$ has source $C^{D \oplus_{c} L} (A \times B) = C^{L} (A \times B) = A \times B$ and target $C^{D} A \times C^{L} B = 1 \times B$ .

Referenced from 5 locations

Categorical Semantics of Coeffects

Interpreting the flat calculus

Definition 150.8 — Interpretation ¶

Fix a cartesian closed $C$ (definition 142.26) with an indexed comonad $C$ carrying the structure of definition 150.6. Interpret base types by a fixed assignment and put $[[C^{s} τ_{1} \to τ_{2}]] : = C^{s} [[τ_{1}]] \Rightarrow [[τ_{2}]]$ ; interpret a context $Γ = x_{1} : τ_{1}, \dots, x_{n} : τ_{n}$ by the product $[[τ_{1}]] \times \dots \times [[τ_{n}]]$ . Interpret derivations by $\begin{aligned} [[Γ @_{f} use ⊢ x_{i} : τ_{i}]] & : = {pr}_{i} \circ ε, \\ [[Γ @_{f} r ⊢ λ x . e : C^{s} τ_{1} \to τ_{2}]] & : = λ ([[Γ, x : τ_{1} @_{f} r \land_{c} s ⊢ e : τ_{2}]] \circ m_{r, s}), \\ [[Γ @_{f} r \oplus_{c} (s ⊛ t) ⊢ e_{1} e_{2} : τ_{2}]] & : = ev \circ ({id}_{} \times [[Γ @_{f} s ⊢ e_{2} : τ_{1} {]]}_{s, t}^{†}) \\ \circ n_{r, s ⊛ t} \circ C^{r \oplus_{c} (s ⊛ t)} Δ, \end{aligned}$ where $Δ : = ⟨ {id}_{}, {id}_{} ⟩$ is the diagonal and $λ (-)$ , $ev$ are the transpose and evaluation of definition 142.26.

Referenced from 8 locations

Categorical Semantics of Coeffects

The application clause is the only one whose shape is not immediate, and it is forced. Both premises need the free variables, so the context is first duplicated inside $C$ by $C^{-} Δ$ ; the duplicate is split by $n$ , whose two indices must be exactly the two premise indices; the argument premise is coextended by $(-)_{s, t}^{†}$ so that its result carries the latent requirement $t$ that the function will consume; and the function premise is applied. Changing any index makes one of the four composites ill typed.

Theorem 150.9 — Soundness of the flat interpretation ¶

Assume the associativity conditions of definition 150.6, and assume subcoeffecting $s \leq r$ is interpreted by a family ${sub}_{s \leq r} : C^{r} A ⟶ C^{s} A$ natural in $A$ and commuting with $ε$ , with $(-)^{†}$ , with $m$ and with $n$ . Then every derivation of the flat calculus has a well-typed interpretation, and two derivations of the same judgment differing only in the placement of subcoeffecting have equal interpretations.

Referenced from 4 locations

Categorical Semantics of Coeffects

Proof of Theorem 150.9 — Soundness of the flat interpretation

Proof. Induction on the derivation.

F-Var. The premise annotation is $use$ , so $ε : C^{use} [[Γ]] ⟶ [[Γ]]$ is available, and ${pr}_{i}$ has the declared type by definition 142.1.

F-Abs. By the induction hypothesis the body is a morphism $C^{r \land_{c} s} ([[Γ]] \times [[τ_{1}]]) ⟶ [[τ_{2}]]$ . Precomposing with $m_{r, s} : C^{r} [[Γ]] \times C^{s} [[τ_{1}]] ⟶ C^{r \land_{c} s} ([[Γ]] \times [[τ_{1}]])$ gives a morphism out of a product, and its transpose under (142.8) has target $C^{s} [[τ_{1}]] \Rightarrow [[τ_{2}]]$ , the interpretation of the declared type.

F-App. By the induction hypotheses the premises are morphisms $C^{r} [[Γ]] ⟶ (C^{t} [[τ_{1}]] \Rightarrow [[τ_{2}]])$ and $C^{s} [[Γ]] ⟶ [[τ_{1}]]$ . Coextending the second at $(s, t)$ gives $C^{s ⊛ t} [[Γ]] ⟶ C^{t} [[τ_{1}]]$ . The composite of definition 150.8 therefore has source $C^{r \oplus_{c} (s ⊛ t)} [[Γ]]$ and target $[[τ_{2}]]$ : the diagonal and $n_{r, s ⊛ t}$ produce the pair of contexts with the two required indices, the product of the two premise morphisms lands in $(C^{t} [[τ_{1}]] \Rightarrow [[τ_{2}]]) \times C^{t} [[τ_{1}]]$ , and $ev$ has the stated target.

Subcoeffecting. The rule composes with ${sub}_{s \leq r}$ , whose type is as declared. The four commutation hypotheses are exactly what is needed to move $sub$ past $ε$ , past a coextension, and past $m$ and $n$ ; moving every occurrence to the root of the derivation gives the second claim.

Well-definedness under associativity. A derivation merging, or splitting, three contexts in two different orders yields two composites differing by the associativity morphism assumed in definition 150.6; that assumption makes them equal. ◻

Remark 150.10 — What soundness does and does not give ¶

Theorem 150.9 says that the interpretation is defined and independent of the derivation. It does not say that it is preserved by reduction: that is theorem 53.2 and theorem 53.5, each proved for its own reduction relation in chapter 53 and neither reproved nor strengthened here. No clause above uses the pure-value premise of the call-by-value card.

Referenced from 2 locations

Categorical Semantics of Coeffects

Recovering the concrete models

Proposition 150.11 — The three models are instances ¶

Each model of section 53.5 is an indexed comonad with the structure of definition 150.6, and its interpretation agrees with definition 150.8.

Liveness: example 150.5 and example 150.7.
Bounded reuse: $S : = N$ with $⊛$ multiplication and unit $1$ , $C^{k} A : = A^{k}$ , counit the projection at $k = 1$ , $m_{j, k}$ pairing componentwise into $(A \times B)^{min (j, k)}$ , and $n_{j, k}$ splitting a tuple of length $max (j, k)$ into its first $j$ and first $k$ entries.
Causal dataflow: $S : = N$ with $⊛$ addition and unit $0$ , $C^{k} A : = A \times A^{k}$ recording the current value and $k$ past ones, counit the first projection, and $m, n$ truncating and duplicating histories.

Referenced from 6 locations

Categorical Semantics of Coeffects

Proof of Proposition 150.11 — The three models are instances

Proof. In each case the three laws (150.1) are checked on elements. For (2), $ε$ at $k = 1$ is the projection $A^{1} \to A$ , and $f_{j, k}^{†}$ applied to a tuple of length $j k$ splits it into $k$ blocks of length $j$ and applies $f$ to each; the third law is the equality of the two ways of blocking a tuple of length $j k t$ , which holds because multiplication is associative. For (3), $ε$ at $k = 0$ is the projection $A \times A^{0} \to A$ , and $f_{j, k}^{†}$ maps a history of length $j + k$ to the history of length $k$ whose entry at position $i$ is $f$ applied to the window of length $j$ ending at $i$ ; the third law is the equality of two windowings, which holds because addition is associative. Agreement with definition 150.8 is then the observation that the clauses of section 53.5 are the displayed composites with these $ε$ , $(-)^{†}$ , $m$ and $n$ substituted. ◻

Exercise 150.1 ¶

★☆☆ Verify the three laws (150.1) for example 150.5 by checking all four index combinations of the third law.

Referenced from 2 locations

Categorical Semantics of Coeffects

Exercise 150.2 ¶

★★☆ Prove that for a one-element index monoid the operation $(-)^{†}$ cannot change the object mapping, and exhibit the clause of example 150.5 that violates the corresponding statement for a two-element monoid.

Referenced from 2 locations

Categorical Semantics of Coeffects

Exercise 150.3 ¶

★★☆ Change $n_{r, s ⊛ t}$ in definition 150.8 to $n_{r ⊛ s, t}$ and show that the composite is no longer well typed, naming the first morphism whose source and target fail to match.

Referenced from 2 locations

Categorical Semantics of Coeffects

The structural calculus, and the boundaries

The structural judgment carries one scalar per variable, so its interpretation replaces the single index $r$ by a vector, and the merge and split families are indexed by vectors: $\begin{aligned} m_{\vec{r}, s} & : C^{\vec{r}} [[Γ]] \times C^{s} [[τ_{1}]] ⟶ C^{(\vec{r}, s)} ([[Γ]] \times [[τ_{1}]]), \\ n_{\vec{r}, \vec{s}} & : C^{\vec{r} \oplus_{c} \vec{s}} (A \times B) ⟶ C^{\vec{r}} A \times C^{\vec{s}} B, \end{aligned}$ where the vector operations act pointwise. The interpretation of S-Abs appends the argument’s scalar to the vector instead of meeting it into a single scalar, and S-App splits pointwise.

Remark 150.12 — The structural soundness statement is separate ¶

Stating the analogue of theorem 150.9 for the structural calculus needs two hypotheses that the flat statement does not: that the pointwise operations satisfy the associativity conditions componentwise, and that the interpretation is stable under exchanging two variables of a context, since the structural rules distinguish positions while the flat rules do not. Those hypotheses are local to the structural card, and no theorem of section 150.4 implies them.

Referenced from 2 locations

Categorical Semantics of Coeffects

Remark 150.13 — The causal-dataflow boundary ¶

Proposition 150.11(3) exhibits causal dataflow as an indexed comonad and does no more. Subject reduction under call-by-name holds for liveness and for bounded reuse. It fails for dataflow. An expression substituted under a binder must carry the history of the position it came from, and ordinary capture-avoiding substitution does not. So a grade algebra by itself supplies no operational semantics and no preservation theorem. The dataflow card owns its own reduction relation, and the call-by-name preservation card restated in convention 150.1 is not available for it.

Referenced from 4 locations

Categorical Semantics of Coeffects

Remark 150.14 — Scope of the name ¶

In this chapter the phrase “indexed comonadic semantics” names the two structures of definition 150.2 and definition 150.6, together with the laws (150.1) and the two associativity conditions. It names nothing else. No theorem of quantitative type theory is proved or used here, and none of graded modal type theory. No result above transfers to a calculus whose contexts carry a different notion of resource.

Referenced from 3 locations

Categorical Semantics of Coeffects

Suggested first pass.

Begin with exercise 150.4 and exercise 150.5, then complete exercise 150.7.

Exercise 150.4 ¶

★★☆ Complete the verification of proposition 150.11(2): write $f_{j, k}^{†}$ explicitly on a tuple of length $j k$ and check the third law of (150.1) for $j = 2$ , $k = 3$ , $t = 2$ by comparing the two blockings of a tuple of length $12$ .

Referenced from 3 locations

Categorical Semantics of Coeffects

Exercise 150.5 ¶

★★☆ Show that $n_{r, s}$ of definition 150.6 cannot in general be inverted: exhibit a model, indices $r, s$ and objects $A, B$ for which $n_{r, s}$ is not a bijection, and say which information is lost.

Referenced from 3 locations

Categorical Semantics of Coeffects

Exercise 150.6 ¶

★★★ For the dataflow model of proposition 150.11(3), take a context supplying one past value and compute $[[λ x . e]]$ by definition 150.8 for a body $e$ that reads the past value. Then compute the interpretation of the term obtained by substituting a context-dependent expression for a variable, and exhibit the two different histories that make remark 150.13 concrete.

Referenced from 2 locations

Categorical Semantics of Coeffects

Exercise 150.7 ¶

★★★ Practical project.indexed-comonad-law-checker Implement a checker for indexed comonads over finite sets. The input is a finite index set with multiplication tables for $⊛$ , $\land_{c}$ and $\oplus_{c}$ and a nominated unit; a carrier assignment sending each index $r$ and each of a finite list of finite sets $A$ to a finite set $C^{r} A$ ; and tables for $ε$ , $(-)_{r, s}^{†}$ , $m_{r, s}$ and $n_{r, s}$ .

Invariant. Before checking any law the program verifies that every supplied table is a total function of the declared source and target, recomputing both from the index arithmetic rather than from the table’s own extent: the source of $f_{r, s}^{†}$ must be $C^{r ⊛ s} A$ , the target of $m_{r, s}$ must be $C^{r \land_{c} s} (A \times B)$ , and the source of $n_{r, s}$ must be $C^{r \oplus_{c} s} (A \times B)$ . It rejects the input, naming the first table whose declared and computed types differ.

Concrete result. For each of the three laws of (150.1) and each of the two associativity conditions of definition 150.6, the program prints either holds or fails together with a witnessing triple of indices and an element of the source at which the two sides differ.

Acceptance test. Run it on the liveness model of example 150.5 and example 150.7 with $A = B = {0, 1}$ : all five checks must print holds. Run it on the bounded-reuse model of proposition 150.11(2) with $A = {0, 1}$ and the index set ${1, 2, 3}$ , which is not closed under $⊛$ : the program must check every triple whose products stay inside the set, print holds for all five, and print the list of triples it skipped together with the product that left the set. A checker that silently omits those triples without reporting them is rejected by this test. Then replace $m_{D, L}$ in the liveness model by $(x, y) \mapsto (x, y)$ and rerun: the type check must reject the input, naming $m_{D, L}$ , because $D \land_{c} L = D$ and the declared target is $C^{D} (A \times B) = 1$ . A run that accepts that replacement has read the target from the table rather than computing it from $\land_{c}$ , which is the defect this test detects.

Referenced from 3 locations

Categorical Semantics of Coeffects

Sources. Definition 150.2 is Definition 2 of T. Petricek, D. Orchard and A. Mycroft, Coeffects: unified static analysis of context-dependence, ICALP 2013 [POM13], physical page 6; lemma 150.3 collects the derived composition and functor action stated on physical pages 6–8 of the same source, and example 150.5 is its Example 2 on physical page 6. Definition 150.6 and the clauses of example 150.7 are on physical page 7; the interpretation of definition 150.8 is its Figure 5 on physical page 8; and the failure of subject reduction for dataflow recorded in remark 150.13 is the discussion following its Theorem 1 on physical page 10. The flat and structural systems restated in convention 150.1, together with the theorem cards this chapter does not reprove, are chapter 53, following Petricek, Orchard and Mycroft [POM14] and the long-form development [Pet17]. The comparison of graded and coeffectful presentations is Liepelt et al. [LMO26]; it is not used above, and remark 150.14 states what this chapter does not claim about it.