Coeffects and Context-Dependent Computation

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

The terms $$e_1=3,e_2=?\mathsf{width}+3$$ can have the same empty effect trace. They do not have the same contextual requirement: $e_2$ needs a binding for the implicit parameter $?\mathsf{width}$. An effect bounds what evaluation does to an environment. A coeffect bounds what evaluation requires from that environment.

Coeffect scalars and the flat judgment

A coeffect scalar structure is a tuple $$(\mathcal{C},⊛,{\oplus }_{\mathsf{c}},\mathsf{use},\mathsf{ign},\le )$$ such that $(\mathcal{C},⊛,\mathsf{use})$ and $(\mathcal{C},{\oplus }_{\mathsf{c}},\mathsf{ign})$ are monoids, $(\mathcal{C},\le )$ is a preorder, and sequential composition distributes over sharing on both sides: $$(r{\oplus }_{\mathsf{c}}s)⊛t=(r⊛t){\oplus }_{\mathsf{c}}(s⊛t),t⊛(r{\oplus }_{\mathsf{c}}s)=(t⊛r){\oplus }_{\mathsf{c}}(t⊛s).$$ The element $\mathsf{use}$ is the requirement of one variable occurrence; $\mathsf{ign}$ is the requirement of an unused binding. The two monoids need not be arithmetic multiplication and addition.

A flat coeffect annotates an entire variable context by one scalar. Choose an operation ${\wedge }_{\mathsf{c}}:\mathcal{C}\times \mathcal{C}\to \mathcal{C}$ satisfying $$\begin{array}{}\text{(}F\text{)}& r{\wedge }_{\mathsf{c}}s\le r{\oplus }_{\mathsf{c}}s.\end{array}$$ The flat judgment is $\mathrm{\Gamma }{@}_{\mathsf{f}}r⊢e:\tau$. Function types carry a latent scalar $\sigma {\stackrel{t}{\to }}_{\mathsf{c}}\tau$. The four rules used below are

$\varnothing {@}_{\mathsf{f}}\mathsf{ign}⊢c:\iota$

$x:\tau {@}_{\mathsf{f}}\mathsf{use}⊢x:\tau$

$\mathrm{\Gamma },x:\sigma {@}_{\mathsf{f}}(r{\wedge }_{\mathsf{c}}s)⊢e:\tau$

$\mathrm{\Gamma }{@}_{\mathsf{f}}r⊢\lambda x.e:\sigma {\stackrel{s}{\to }}_{\mathsf{c}}\tau$

${\mathrm{\Gamma }}_1{@}_{\mathsf{f}}r⊢e_1:\sigma {\stackrel{t}{\to }}_{\mathsf{c}}\tau$${\mathrm{\Gamma }}_2{@}_{\mathsf{f}}s⊢e_2:\sigma$

${\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2{@}_{\mathsf{f}}(r{\oplus }_{\mathsf{c}}(t⊛s))⊢e_1{e}_2:\tau$

Weakening, exchange, contraction, and subcoeffecting are admissible when the selected flat algebra validates their corresponding context transformations. Condition $F$ is the exact inequality used by beta preservation.

For implicit parameters take $$\mathcal{C}=\mathcal{P}(\mathsf{Name}\times \mathsf{Type}),⊛={\oplus }_{\mathsf{c}}={\wedge }_{\mathsf{c}}=\cup ,\mathsf{use}=\mathsf{ign}=\varnothing ,\le =\subseteq .$$ The primitive access judgment is $$\mathrm{\Gamma }{@}_{\mathsf{f}}\{(?p,\tau )\}⊢?p:\tau .$$ Thus the opening terms have requirements $\varnothing$ and $\{(?\mathsf{width},\mathsf{int})\}$, although both are effect free.

The flat call-by-value card

The first theorem card uses the flat rules just printed and call-by-value beta reduction. A syntactic value $v$ is a pure value when it has a derivation $\mathrm{\Gamma }{@}_{\mathsf{f}}\mathsf{use}⊢v:\sigma$. In the flat shape there is one scalar regardless of the number of variables in $\mathrm{\Gamma }$.

Proof of Lemma 53.1 — Flat call-by-value substitution

Proof. Induct on the derivation of the receiving term $e_r$. In the variable case $e_r=x$, the premise annotation is $\mathsf{use}$, so the substituted derivation is the first hypothesis. A different variable retains its own F-Var derivation and weakens across $\mathrm{\Gamma }$. In an abstraction, choose its binder outside $\mathrm{fv}(e_s)\cup \mathrm{dom}({\mathrm{\Gamma }}_1,\mathrm{\Gamma },{\mathrm{\Gamma }}_2)$; the induction hypothesis checks the renamed body and F-Abs restores the same immediate and latent scalars. In an application, apply the induction hypothesis to both premises in which $x$ occurs. Distributivity of $⊛$ over ${\oplus }_{\mathsf{c}}$ reconstructs the annotation in F-App. The context-transformation cases use the corresponding flat algebra law. These cases exhaust the derivation. ◻

Proof of Theorem 53.2 — Flat call-by-value subject reduction

Proof. The congruence cases rebuild their typing rules. For beta, invert F-App and F-Abs. The value premise has scalar $\mathsf{use}$, so lemma 53.1 types the reduct. The two static context combinations differ by replacing $r{\wedge }_{\mathsf{c}}s$ by $r{\oplus }_{\mathsf{c}}s$; condition $F$ and subcoeffecting give the required annotation. This is Theorem 11 of the selected calculus [POM14]. ◻

If beta contracts an arbitrary context-dependent argument, the substitution lemma’s pure-value premise is false. The call-by-value theorem therefore does not justify call-by-name evaluation.

The flat call-by-name card

The second card keeps the flat typing rules but changes the reduction relation. A flat algebra is top-pointed when $s\le \mathsf{use}$ for every $s\in \mathcal{C}$. It is bottom-pointed when $\mathsf{use}\le s$ for every $s\in \mathcal{C}$.

Proof of Lemma 53.3 — Top-pointed substitution

Proof. Top-pointedness gives $s\le \mathsf{use}$. Subcoeffecting retypes $e_s$ at $\mathsf{use}$, so lemma 53.1 applies. ◻

Proof of Lemma 53.4 — Bottom-pointed substitution

Proof. Induct on the receiving derivation. The $x$-case uses $\mathsf{use}\le s$ and subcoeffecting. Application combines each copy of the substituted requirement with the surrounding requirement. Commutativity reassociates $s$ with the free-variable context; idempotence merges repeated copies introduced by contraction. Abstraction preserves that combined requirement because ${\wedge }_{\mathsf{c}}=⊛={\oplus }_{\mathsf{c}}$. ◻

Proof of Theorem 53.5 — Flat call-by-name subject reduction

Proof. Congruence preserves the derivation. In the beta case, inversion of F-App and F-Abs produces the premises of the appropriate substitution lemma. The top-pointed lemma retains $r$. In the bottom-pointed case, the equality of the three operations and idempotence reduce the substituted annotation to the one in the application conclusion. This is the two-case hypothesis of source Theorem 14 [POM14], not a result for an arbitrary flat algebra. ◻

The implicit-parameter instance is bottom-pointed under inclusion because $\mathsf{use}=\varnothing$, and its three operations are set union. Hence the call-by-name theorem applies. Flat liveness instead uses a greatest $\mathsf{use}$ and belongs to the top-pointed case.

The structural card

A structural coeffect assigns one scalar to each variable. A context $x_1:{\tau }_1,\dots ,x_n:{\tau }_n$ carries a vector $R=⟨r_1,\dots ,r_n⟩\in {\mathcal{C}}^n$. The empty vector is $⟨⟩$, vector concatenation is $R++S$, and scalar multiplication is pointwise: $$r⊛⟨s_1,\dots ,s_n⟩=⟨r⊛s_1,\dots ,r⊛s_n⟩.$$ The judgment is $\mathrm{\Gamma }{@}_{\mathsf{s}}R⊢e:\tau$. Its abstraction and application rules are

$\mathrm{\Gamma },x:\sigma {@}_{\mathsf{s}}(R++⟨s⟩)⊢e:\tau$

$\mathrm{\Gamma }{@}_{\mathsf{s}}R⊢\lambda x.e:\sigma {\stackrel{s}{\to }}_{\mathsf{c}}\tau$

${\mathrm{\Gamma }}_1{@}_{\mathsf{s}}R⊢e_1:\sigma {\stackrel{t}{\to }}_{\mathsf{c}}\tau$${\mathrm{\Gamma }}_2{@}_{\mathsf{s}}S⊢e_2:\sigma$

${\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2{@}_{\mathsf{s}}(R++(t⊛S))⊢e_1{e}_2:\tau$

Variables carry $⟨\mathsf{use}⟩$. Weakening appends $⟨\mathsf{ign}⟩$. Exchange swaps a variable and its scalar. Contraction replaces adjacent scalars $r,s$ by $r{\oplus }_{\mathsf{c}}s$. Write ${\mathrm{\Gamma }}^{\prime }{@}_{\mathsf{s}}{R}^{\prime }{⇝}_{\mathsf{ctx},\theta }\mathrm{\Gamma }{@}_{\mathsf{s}}R$ for the context-transformation package generated by these four operations. The package is locally sound when every generator transforms a typing derivation as stated, and locally complete when every weakening, adjacent permutation, adjacent identification, or pointwise increase used in a derivation factors through those generators. The structural card assumes both properties, together with the two scalar monoids and both distributivity equations from section 53.1. This states exactly what the contextual rule may do; it is not an unrestricted structural congruence.

Proof of Lemma 53.6 — Structural substitution

Proof. Induct on the receiving derivation. The variable case $x$ has $r=\mathsf{use}$, and the sequential monoid identity gives $\mathsf{use}⊛S=S$. Abstraction extends both the context and vector at the same end; alpha-renaming chooses its binder outside $\mathrm{fv}(e_s)\cup \mathrm{dom}({\mathrm{\Gamma }}_1,\mathrm{\Gamma },{\mathrm{\Gamma }}_2)$. Application substitutes into each premise and uses distributivity to combine multiple occurrences. Weakening, exchange, and contraction transform the variable and its scalar together; the stated local soundness/completeness conditions reconstruct those rules. No flat operation ${\wedge }_{\mathsf{c}}$ occurs. ◻

Proof of Theorem 53.7 — Structural subject reduction

Proof. The beta case inverts S-App and S-Abs; the bound variable occupies one unique vector position. Applying lemma 53.6 replaces its scalar $r$ by $r⊛S$, exactly the vector printed by S-App. Congruence cases rebuild their derivations. Context conversions before or after the redex are transported by local soundness and completeness of weakening, exchange, and contraction. This is source Theorem 8 at the structural signature [POM14]. ◻

For bounded reuse choose $$(\mathbb{N},\times ,+,1,0,\le ).$$ The term $\lambda x.x+x$ assigns latent grade $2$ to $x$, because the two occurrences contract $1+1$. Applying it to $y$, whose vector is $⟨1⟩$, produces $2\times ⟨1⟩=⟨2⟩$. This is a contextual demand on $y$, not a claim that evaluation performs two effects.

Set models and a dataflow boundary

The implicit-parameter model can be constructed without categorical machinery. Regard every object $A$ as a set. A requirement set is well formed when it assigns at most one type to each name. A finite typed dictionary $\rho$ realizes $R$, written $\rho {\vDash }_{\mathsf{d}}R$, when $\rho (?p)\in \tau$ for every $(?p,\tau )\in R$. Let $$D_R(A)=\{(\rho ,a)\mid \rho \text{ is a finite typed dictionary},\rho {\vDash }_{\mathsf{d}}R,a\in A\}.$$ For $R\subseteq S$, let $\rho {|}_R$ retain exactly the dictionary entries named in $R$, and define the requirement-forgetting map $${\mathrm{res}}_R^S:D_S(A)⟶D_R(A),{\mathrm{res}}_R^S(\rho ,a)=(\rho {|}_R,a).$$ If $(\rho ,(a,b))\in D_{R\cup S}(A\times B)$, then $$(\rho ,(a,b))⟶((\rho {|}_R,a),(\rho {|}_S,b))\in D_R(A)\times D_S(B).$$ The two restricted dictionaries are available because $\rho$ realizes every entry in $R\cup S$. For an access $(?p)$, the map sends $(\rho ,\ast )$ to $\rho (?p)$; its domain condition is exactly $(?p,\tau )\in R$.

The bounded-reuse model is also concrete. For $R=⟨r_1,\dots ,r_n⟩$, set $$B_R(A_1,\dots ,A_n)=A_1^{r_1}\times \cdots \times A_n^{r_n}.$$ The variable rule selects the sole component of $A^1$. Contraction uses the canonical regrouping $A^r\times A^s\cong A^{r+s}$. Substitution uses $(A^s{)}^r\cong A^{r\times s}$, which is the semantic counterpart of the grade $r⊛s$ in lemma 53.6.

Causal dataflow needs a different operational account. Let a stream environment $\rho$ map each $x$ to values $\rho (x{)}_0,\rho (x{)}_1,\dots$. The dedicated lookup rule is $$⟨{\mathsf{prev}}^{k}x,\rho ,n⟩{⟶}_{\mathsf{df}}\rho (x{)}_{n-k}(k\le n).$$ A structural vector $R$ is sound for this lookup fragment when every occurrence ${\mathsf{prev}}^k{x}_i$ has $k\le R_i$. Ordinary syntactic substitution is unsuitable as the operational definition: replacing $x$ by an arbitrary stream expression can duplicate or shift the history demanded by that expression, whereas the machine rule reads a named stream at an explicit time index. The chapter therefore claims only the displayed lookup bound and its immediate closure under arithmetic contexts. It does not claim an independent progress, preservation, or cache-optimality theorem for a complete dataflow language.

The non-transfer boundary can now be read without identifying the cards:

The dictionary and finite-power constructions prove only the displayed local Set calculations. They do not yet supply the indexed comonad, its counit and comultiplication, or the coherence equations needed for a categorical model of all three cards. That construction must wait until those categorical notions have been developed.

Sources.

The earlier unified flat calculus introduces implicit parameters, liveness, and dataflow under one whole-context annotation and supplies the indexed comonadic account [POM13]. It is provenance for the flat motivation, not for the later structural theorem. The archived Petricek–Orchard–Mycroft PDF pages 4–6 print Definitions 1–5 and the structural and flat instances; pages 7–8 print structural substitution, Theorems 8, 11, and 14, and their exact call-by-value, top-pointed, and bottom-pointed hypotheses [POM14]. The longer thesis supplies worked implicit-parameter and dataflow derivations, not a license to move results between the cards [Pet17].