Two Bases for Graded Types: Calculi and Correspondence

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

Suppose $f$ uses its argument with grade $r$. In the body $f(fx)$, the outer occurrence of $f$ contributes $1$, the inner occurrence lies in an argument scaled by $r$, and $x$ lies under both applications. Their grades are therefore $1+r$ and $r\cdot r$. There are two places to record those facts. A judgment may grade the assumptions for $f$ and $x$, or a type may place a graded box around the argument of $f$. The annotations look interchangeable. They are not: one presentation has graded functions, while the other has linear functions and a graded modality. This chapter fixes the two nondependent calculi of Liepelt, Marshall, and Orchard and proves only the translations they establish [LMO26].

One algebra, two bases

Fix a preordered semiring $R,0,1,+,\cdot ,{⊑}_{\mathsf{q}}$. Addition and multiplication are monotone, with respective units $0$ and $1$. A graded assumption is written $x{:}_{r}A$, while a linear assumption is written $x:A$. Context addition and scalar multiplication are pointwise: $$(\mathrm{\Delta },x{:}_{r}A)+({\mathrm{\Delta }}^{\prime },x{:}_{s}A)=\mathrm{\Delta }+{\mathrm{\Delta }}^{\prime },x{:}_{r+s}A,q\cdot (\mathrm{\Delta },x{:}_{r}A)=q\cdot \mathrm{\Delta },x{:}_{q\cdot r}A.$$ Missing variables carry grade $0$. These equations describe annotations; they do not yet say whether a grade is an exact count, an upper bound, a sensitivity, or a security level. That interpretation is fixed by the chosen semiring and preorder.

Linear Base

The Linear Base puts ordinary functions over a context containing linear and graded assumptions: $$A,B::=K\mid A⊸B\mid {◻}_{r}A,t,u::=x\mid \lambda x.t\mid tu\mid [t]\mid \mathsf{let}[x]=t\mathsf{in}u.$$ Write $\mathrm{\Gamma }{⊢}_{\mathsf{L}}t:A$. The notation $\mathrm{gr}(\mathrm{\Gamma })$ means that every assumption in $\mathrm{\Gamma }$ is graded, while ${\mathrm{gr}}_0(\mathrm{\Gamma })$ means that each has grade $0$. The complete typing rules are

$x:A{⊢}_{\mathsf{L}}x:A$

$\mathrm{\Gamma },x:A{⊢}_{\mathsf{L}}t:B$

$\mathrm{\Gamma }{⊢}_{\mathsf{L}}\lambda x.t:A⊸B$

${\mathrm{\Gamma }}_1{⊢}_{\mathsf{L}}t:A⊸B$${\mathrm{\Gamma }}_2{⊢}_{\mathsf{L}}u:A$

${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2{⊢}_{\mathsf{L}}tu:B$

$\mathrm{\Gamma }{⊢}_{\mathsf{L}}t:A$${\mathrm{gr}}_0({\mathrm{\Gamma }}^{\prime })$

$\mathrm{\Gamma }+{\mathrm{\Gamma }}^{\prime }{⊢}_{\mathsf{L}}t:A$

$\mathrm{\Gamma },x:A{⊢}_{\mathsf{L}}t:B$

$\mathrm{\Gamma },x:[A{]}_1{⊢}_{\mathsf{L}}t:B$

$\mathrm{\Gamma }{⊢}_{\mathsf{L}}t:A$$\mathrm{gr}(\mathrm{\Gamma })$

$r\cdot \mathrm{\Gamma }{⊢}_{\mathsf{L}}[t]:{◻}_{r}A$

${\mathrm{\Gamma }}_1{⊢}_{\mathsf{L}}t:{◻}_{r}A$${\mathrm{\Gamma }}_2,x:[A{]}_r{⊢}_{\mathsf{L}}u:B$

${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2{⊢}_{\mathsf{L}}\mathsf{let}[x]=t\mathsf{in}u:B$

$\mathrm{\Gamma },x:[A{]}_r{⊢}_{\mathsf{L}}t:B$$r{⊑}_{\mathsf{q}}s$

$\mathrm{\Gamma },x:[A{]}_s{⊢}_{\mathsf{L}}t:B$

Context addition is undefined when both operands contain the same linear assumption; only shared graded assumptions are added. Thus there is no contraction rule for a linear assumption. Promotion scales an entire graded context; it cannot close over a linear assumption.

Call-by-name reduction has the two principal steps $$(\lambda x.t)u{⟶}_{\mathsf{L}}t[u/x],\mathsf{let}[x]=[t]\mathsf{in}u{⟶}_{\mathsf{L}}u[t/x],$$ and congruence in function and scrutinee position. Its reflexive transitive closure is ${⟶}_{\mathsf{L}}^{\ast }$.

Graded Base

The Graded Base grades the domain of every function: $$A,B::=K\mid A\stackrel{r}{\to }B,t,u::=x\mid \lambda x.t\mid tu.$$ Every assumption is graded. The complete judgment $\mathrm{\Delta }{⊢}_{\mathsf{G}}t:A$ is generated by

$x{:}_{1}A{⊢}_{\mathsf{G}}x:A$

$\mathrm{\Delta }{⊢}_{\mathsf{G}}t:A$

$\mathrm{\Delta },0\cdot {\mathrm{\Delta }}^{\prime }{⊢}_{\mathsf{G}}t:A$

$\mathrm{\Delta },x{:}_{r}A{⊢}_{\mathsf{G}}t:B$$r{⊑}_{\mathsf{q}}s$

$\mathrm{\Delta },x{:}_{s}A{⊢}_{\mathsf{G}}t:B$

$\mathrm{\Delta },x{:}_{r}A{⊢}_{\mathsf{G}}t:B$

$\mathrm{\Delta }{⊢}_{\mathsf{G}}\lambda x.t:A\stackrel{r}{\to }B$

${\mathrm{\Delta }}_1{⊢}_{\mathsf{G}}t:A\stackrel{r}{\to }B$${\mathrm{\Delta }}_2{⊢}_{\mathsf{G}}u:A$

${\mathrm{\Delta }}_1+r\cdot {\mathrm{\Delta }}_2{⊢}_{\mathsf{G}}tu:B$

The principal reduction is $(\lambda x.t)u{⟶}_{\mathsf{G}}t[u/x]$; congruence is in function position. Thus both bases use call by name.

Proof of Lemma 54.2 — Graded substitution

Proof. Induct on the first derivation. In the variable case for $x$, the context has grade $1$, so the conclusion is the second premise. Another variable uses G-Weak. The abstraction case applies the induction hypothesis under the binder. In the application case, write the function’s arrow grade as $q$, and write the grades of $x$ in the function and argument premises as $a$ and $b$. The conclusion before substitution has context ${\mathrm{\Delta }}_1+q{\mathrm{\Delta }}_2,x{:}_{a+qb}A$. The two induction hypotheses produce ${\mathrm{\Delta }}_1+a\mathrm{\Theta }$ and ${\mathrm{\Delta }}_2+b\mathrm{\Theta }$; rule G-App combines them as $$({\mathrm{\Delta }}_1+a\mathrm{\Theta })+q({\mathrm{\Delta }}_2+b\mathrm{\Theta })={\mathrm{\Delta }}_1+q{\mathrm{\Delta }}_2+(a+qb)\mathrm{\Theta },$$ by distributivity and associativity. Weakening and approximation commute with substitution by monotonicity of addition and multiplication. ◻

For $h=\lambda f.\lambda x.f(fx)$, the outer use of $f$ has grade $1$, its inner use is scaled by $r$, and the nested argument grades multiply: $${⊢}_{\mathsf{G}}h:(A\stackrel{r}{\to }A)\stackrel{1+r}{\to }A\stackrel{r\cdot r}{\to }A.$$ This single derivation separates addition for independent occurrences from multiplication for nested demand. The printed Examples 2.13–2.14 of the source show (1+1) for the grade of (f). Rule G-App, however, scales the inner occurrence by the arbitrary arrow grade (r), giving (1+r); the chapter uses that rule-derived correction throughout [LMO26].

The algebra decides what that calculation means. The following four instantiations use the same syntax but not the same theorem:

The exact-use and security rows are instances exhibited by the source; the upper-bound and sensitivity rows are direct semiring calculations. The security derivation does not by itself prove noninterference, and the sensitivity row does not by itself define a metric semantics. The bounded-use and Level-security examples in Granule illustrate the same requirement to fix the algebra before reading an annotation; they do not supply a theorem for the two bases [OLI19].

From Graded Base to Linear Base

The direct translation inserts a box at every graded domain: where $y$ is fresh. Context translation is pointwise and consequently commutes with addition and scaling.

Proof of Theorem 54.3 — Graded-to-linear correspondence

Proof. For item 1, induction on typing. The only new cases are abstraction and application. Abstraction translates its graded assumption into $x:[\mathcal{L}[[A]]{]}_r$, eliminates it with L-Let, and then applies L-Abs. Application promotes the translated argument with L-Prom and combines contexts with L-App. The identity $\mathcal{L}[[r\cdot \mathrm{\Delta }]]=r\cdot \mathcal{L}[[\mathrm{\Delta }]]$ supplies the required context.

For item 2, the principal calculation is The congruence case follows from function-position congruence. Item 3 is an induction over the source equational derivation; the beta case is the displayed calculation, and congruence and equivalence rules are homomorphic. These are the three clauses of Theorem 1 of the source; its Appendix B.1 gives the standard weakening and substitution details [LMO26]. ◻

Proof of Corollary 54.4 — Grade preservation

Proof. Both equations follow pointwise from $\mathcal{L}[[x{:}_{q}A]]=x:[\mathcal{L}[[A]]{]}_q$. ◻

The converse is false as a direct translation. A term of type $A\stackrel{1}{\to }B$ does not promise exactly one use: in a semiring where $0=1$, the grade carries no such information. Mapping it to $A⊸B$ would manufacture linearity. The source therefore uses continuation passing.

From Linear Base to Graded Base by continuations

Fix an answer type $K$. The call-by-name CPS translation is A linear assumption maps to grade $1$; $x:[A{]}_r$ maps to grade $r$. The continuation is essential: it supplies the multiplication needed to simulate promotion and unboxing.

Proof of Theorem 54.5 — Linear-to-graded CPS correspondence

Proof. Typing is by induction on the Linear Base derivation. Linear variables use grade $1$; L-Prom becomes multiplication of the translated context by $r$; and L-Let becomes graded substitution. The beta simulations are finite full-beta calculations through the displayed continuations. The modal beta calculation substitutes the value passed to the continuation; modal eta cancels the continuation introduced for a box. Function eta is excluded because the CPS type is not definitionally an unboxed function type. This is exactly Theorem 2 and its stated equation boundary in the source; Appendix B.2 verifies every remaining rule case [LMO26]. ◻

Neither theorem asserts inverse translations, full abstraction, normalization, or a common denotational semantics. Products make the limit concrete: a negative-position product in the continuation translation is not the direct image of a Graded Base product. Similar-looking grades therefore support a correspondence, not an identification of calculi.

A separate effect–coeffect calculus

Gaboardi, Katsumata, Orchard, Breuvart, and Uustalu combine effects and coeffects in a third calculus [GyKO^+16]. It is not a corollary of either translation above. Fix an effect preordered monoid $E,1,\bullet$, a coeffect preordered semiring $R$, a distributive-law format $\varphi$, and the source’s matched-pair operations connecting the two grades. The type grammar is $$A,B::=o\mid A\to B\mid T_{e}A\mid D_{r}A.$$ The type $T_{e}A$ classifies a computation with effect grade $e$; the type $D_{r}A$ classifies data made available with coeffect grade $r$. A judgment has linear assumptions $x:A$ and discharged assumptions $x:[A{]}_r$. Context sum is defined only when repeated variables are discharged, in which case their grades add. Scalar multiplication $r\ast [\mathrm{\Gamma }]$ is defined only for a fully discharged context. Here is the complete typing card:

$x:A⊢x:A$

$\mathrm{\Gamma }⊢t:A$

${\mathrm{\Gamma }}^{\prime },[\mathrm{\Delta }{]}_0⊢t:B$

$\mathrm{\Gamma },x:A⊢t:B$

$\mathrm{\Gamma }⊢\lambda x.t:A\to B$

$\mathrm{\Gamma }⊢t:A\to B$$\mathrm{\Delta }⊢u:A$

$\mathrm{\Gamma }+\mathrm{\Delta }⊢tu:B$

$\mathrm{\Gamma }⊢t:A$

$\mathrm{\Gamma }⊢⟨t⟩:T_{1}A$

$\mathrm{\Gamma }⊢t_1:T_{e}A$$\mathrm{\Delta },x:A⊢t_2:T_{f}B$

$\mathrm{\Gamma }+\mathrm{\Delta }⊢\mathsf{let}⟨x⟩=t_1\mathsf{in}{t}_2:T_{e\bullet f}B$

$\mathrm{\Gamma },x:A⊢t:B$

$\mathrm{\Gamma },x:[A{]}_1⊢t:B$

$[\mathrm{\Gamma }]⊢t:B$

$r\ast [\mathrm{\Gamma }]⊢[t]:D_{r}B$

$\mathrm{\Gamma }⊢t_1:D_{r}A$$\mathrm{\Delta },x:[A{]}_r⊢t_2:B$

$\mathrm{\Gamma }+\mathrm{\Delta }⊢\mathsf{let}[x]=t_1\mathsf{in}{t}_2:B$

$⊢{\mathsf{dist}}_{r,e}^{\varphi }:F_{r,e}^{\varphi }A\to G_{r,e}^{\varphi }A$

$⊢\mathsf{op}:A_{\mathsf{op}}$

Subtyping is covariant in effect grades and contravariant in coeffect grades: Arrow subtyping and pointwise context subtyping complete the relation. The eight choices of $F_{r,e}^{\varphi }$ and $G_{r,e}^{\varphi }$ are the source’s four left/right information-flow formats crossed with the choices $T$-over-$D$ and $D$-over-$T$; choosing one is part of fixing the calculus, not a derived equivalence.

One completely typed program exposes both coordinates. Assume $d:D_{2}A$, $p:A\to T_{e}B$, and $c:A\to B\to C$. Then $$\mathsf{let}[x]=d\mathsf{in}\mathsf{let}⟨y⟩=px\mathsf{in}⟨cxy⟩:T_{e}C.$$ The first occurrence of $x$ types $px:T_{e}B$; the second types $cxy:C$. Each premise derives $x:[A{]}_1$, so EC-LetT adds them to $x:[A{]}_2$, exactly the discharged assumption required by EC-LetD. The effect coordinate is instead $e\bullet 1=e$. Thus the coeffect addition $1+1=2$ accounts for two contextual uses while effect multiplication composes the producer with a pure continuation. Neither coordinate is a Koka effect row or a QTT usage annotation.

Proof of Lemma 54.6 — Two substitution principles

Proof. These are Lemmas 1 and 2 of the source. Induction on the first derivation proves both. The linear variable case replaces one assumption by $\mathrm{\Delta }$. The discharged variable case replaces grade $r$ by $r\cdot \mathrm{\Delta }$. The modal introduction case is valid only because its premise has a fully discharged context. Every other rule follows from distributivity and monotonicity. ◻

Orienting the calculus’s typed equations gives an operational reduction relation for the fragment without primitive operations. Every oriented equation has the same type and context on both sides. The pure beta rule uses linear substitution; the coeffect beta rule uses coeffectful substitution; effect beta and associativity use the effect-monoid laws; the distributive rules use the fixed matched-pair equations. Hence each principal step preserves its judgment. This is the source’s type-preservation argument for the oriented equations, not a progress theorem. The published semantic theorem is different:

Proof of Theorem 54.7 — Equational soundness of combined grading

Proof. Induct on the equality derivation. Congruence cases use functoriality. The beta cases use the two substitution lemmas, interpreted respectively by ordinary composition and the graded action. Unit and associativity equations use the monoid and semiring coherence maps; the distributive equation uses the specified interaction between $T_e$ and $D_r$. This is Theorem 1 of Gaboardi et al.; its statement is denotational soundness, not progress [GyKO^+16]. ◻

Optional route.

Chapter 47.

Fractional ownership through graded uniqueness$\star$

Marshall and Orchard’s fractional-uniqueness calculus assigns reference permissions from a semiring, but adds heaps, borrowing, and uniqueness conditions not present in the two bases above [MO24a]. It permits several read-only fractional references whose incoming permissions sum to $1$, while an in-place update requires one reference carrying permission $1$.

For the reference occurrences in a term $t$ that target identifier $id$ in heap $H$, write $$P(t,H,id)=\sum _{\begin{array}{c}\rho \in \mathsf{refs}(t)\\ \rho {\mapsto }_{p}id\in H\end{array}}p.$$ This abbreviation exposes the heap hypotheses of the source theorems; it is not a Graded Base context grade.

Proof of Theorem 54.8 — Fractional-uniqueness safety package

Proof. The five clauses are imported at their exact source signatures. Progress is by typing induction and heap compatibility. Preservation couples substitution with heap evolution; the non-function payload restriction is used when a stored value is recovered. Borrow safety is an invariant on the sum of permissions targeting each location. Induction over ${{⇝}_{\mathsf{fu}}}^{\ast }$ gives the multistep clause, from which uniqueness is immediate. Equational soundness then uses preservation plus confluence of the fully dereferenced term theory. The source’s Sections 6.2–6.4 contain the case analysis; none of these statements is transferred to Linear Base or Graded Base. ◻

The pinned Granule 0.9.5.0 evaluator makes the ownership distinction executable. Loading examples.gr accepts $\mathsf{exampleBorrow}:\ast \mathsf{Colour}\to \ast \mathsf{Colour}$, whose borrow is split into two fractional observations and joined before the unique value is returned. Loading parsum.gr accepts It then evaluates the parallel shared reads followed by the full-permission reference update to $100.0$. Appendix E records the preserved image, exact commands, and hashes. This is implementation evidence for the language design, not a machine-checked proof of theorem 54.8. The chapter’s Kappa supplement checks only a finite grade-correspondence model.

What each result says

Exact-use, upper-bound, sensitivity, and security readings are therefore examples only when their algebra validates the required order and operations. The translations preserve the written grades; they do not choose their meaning.

Chapter 53 also grades contextual requirements. The named bridge used here is corollary 54.4: the direct translation preserves the same semiring coefficient while moving it from an assumption to a box, and the CPS translation preserves it in the reverse direction. This compares contextual requirements with usage accounting at the two frozen nondependent signatures; it does not transfer a substitution or subject-reduction theorem from chapter 53.

Dependency creates the next obstruction. If a result type $B(x)$ mentions a graded input, substitution must transport $B(u)$ as well as scale the term context. Linear Base elimination above acts only in terms, and the reverse translation fixes a nondependent answer type $K$; neither correspondence theorem licenses eliminating a graded box into a type or continuation-encoding a dependency. A quantitative dependent calculus therefore needs its own judgments and metatheory.

Sources and theorem boundary

The two-base calculi and Theorems 1–2 come from the ICFP 2026 paper and its extended Appendices B.1–B.2 [LMO26]. Lemmas 1–2 of Section 3 and Theorem 1 of Section 5 supply the combined substitutions and soundness theorem [GyKO^+16]. The fractional route uses Progress 6.6, Preservation 6.7, Borrow Safety Lemma 6.8, Borrow Safety Theorem 6.9, Uniqueness Corollary 6.10, and Equational Soundness Theorem 6.11 of Marshall and Orchard [MO24a]. None of these results turns arbitrary semiring grades into cost, sensitivity, information-flow, or ownership guarantees.