Quantitative Dependent Type Theory

Prerequisites. Direct starred prerequisites: Chapter 20, Chapter 40. No later core chapter depends on this route.

The indices $0,1,\omega$ distinguish absence, exact use, and unrestricted use, but the previous chapter fixes those three quantities in advance. It cannot state that a variable is used twice, that a branch costs $r$, or that substitution multiplies one demand by another. Ordinary dependent typing has the opposite defect: an index may occur in a type without recording whether it survives at run time.

A quantitative judgment puts both facts in one place. Types see the whole context spine; annotations record computational demand. The annotation zero therefore means “available to type formation but absent from this computation.” It does not mean that every two inhabitants of the annotated type are propositionally equal.

Semiring-indexed contexts

The natural numbers, the Boolean semiring, and the zero–one–many semiring are examples. Positivity is used when a conclusion has quantity zero: it lets the proof recover that every summand was zero. The zero-product property is used in substitution: if a scaled demand vanishes, either the outer demand or the substituted computation’s demand vanishes.

Allowing an arbitrary output quantity looks more general, but it breaks substitution for the zero–one–many semiring. A term can coerce a function that uses its argument once to one announced at usage $\omega$. Substituting that function into a context split requiring $\omega =1+\omega$ would require splitting an actual usage-one derivation into usage $1$ and $\omega$, which is impossible. Restricting the output to zero or one prevents this hidden subusage step.

Proof of Lemma 99.3 — Zero needs nothing

Proof. Induct on the typing derivation. A variable derivation at output zero has a zero context by its rule. In every rule that adds premise contexts, the conclusion annotations are sums; positivity forces each summand to be zero. In every rule that scales a premise context, the conclusion annotations are products; the zero-product property separates a zero output multiplier from a zero premise annotation. Constants contribute the zero context. These are all ways in which an annotation enters a conclusion. ◻

The converse is false. A closed Boolean constant can be classified at output quantity one while requiring the zero context. Thus the lemma detects absence of input demand; it does not reconstruct the output quantity.

Dependent quantitative rules

The variable rule exposes both output fragments:

$0\mathrm{\Gamma },x{:}^{\sigma }S,0{\mathrm{\Gamma }}^{\prime }⊢$

$0\mathrm{\Gamma },x{:}^{\sigma }S,0{\mathrm{\Gamma }}^{\prime }⊢x{:}^{\sigma }S$

where $\sigma \in \{0,1\}$. At output one it consumes one copy; its erased counterpart is available in a zero context. Function application then performs the semiring calculation visible in its conclusion. If a function uses its argument three times and the argument uses resources $2\mathrm{\Delta }$, the application contributes $3(2\mathrm{\Delta })=6\mathrm{\Delta }$.

Substitution multiplies demand

Proof of Theorem 99.6 — Quantitative substitution

Proof. Prove context formation, type formation, terms, and equalities simultaneously. The variable case makes the context formula necessary. When the selected variable is $x$, its use is $\rho$, so replacing it by $N$ demands $\rho {\mathrm{\Gamma }}_2$. When another variable is selected, $x$ has zero demand in that branch and contributes $0{\mathrm{\Gamma }}_2$.

For QTT-App, alpha-rename its binder to $y$ and write the application as $LM$, with result type $T[M/y]$. Split the demand $\rho$ on the substituted variable $x$ between the function and argument derivations as ${\rho }_1+\pi {\rho }_2$. The induction hypotheses give the contexts ${\mathrm{\Delta }}_1+{\rho }_1{\mathrm{\Gamma }}_2$ and ${\mathrm{\Delta }}_2+{\rho }_2{\mathrm{\Gamma }}_2$. Rebuilding the rule yields The rebuilt type is $T[N/x][M[N/x]/y]$, equal to $T[M/y][N/x]$ by capture-avoiding substitution composition.

For QTT-Lam, alpha-rename the binder and use $\rho (\sigma \pi )=(\rho \sigma )\pi$ to rebuild its body demand. The pair case uses distributivity in the same direction as application. In QTT-Let, split the substituted variable’s demand between the scrutinee and body premises as ${\rho }_1+{\rho }_2$. The induction hypotheses yield ${\mathrm{\Delta }}_1+{\rho }_1{\mathrm{\Gamma }}_2$ and ${\mathrm{\Delta }}_2+{\rho }_2{\mathrm{\Gamma }}_2$; rebuilding the exact rule gives their sum, which is ${\mathrm{\Delta }}_1+{\mathrm{\Delta }}_2+({\rho }_1+{\rho }_2){\mathrm{\Gamma }}_2$ by associativity and commutativity. The zero-spine premise is preserved by clause (1), and capture-avoiding composition identifies $U[P/z][N/x]$ with $U[N/x][P[N/x]/z]$. Formation and equality cases use clause (1); constants and unit constructors contribute zero. Positivity and the zero-product property discharge the side conditions in precisely the branches where an output quantity is zero. Every rule is therefore reconstructed with the displayed context. ◻

The multiplication $\rho {\mathrm{\Gamma }}_2$ is not optional bookkeeping. Replacing it by ${\mathrm{\Gamma }}_2$ undercounts an argument used twice; replacing it by $\rho +{\mathrm{\Gamma }}_2$ is ill sorted because $\rho$ is a scalar and ${\mathrm{\Gamma }}_2$ is a vector of demands.

Proof of Corollary 99.7 — Beta preservation

Proof. Invert QTT-App and QTT-Lam. Their contexts expose exactly the two premises and the scalar $\rho$ required by theorem 99.6(2). Apply that theorem for the root beta step. For a compatible step, induct on the one-hole term context, use the induction hypothesis for its changed premise, and rebuild the enclosing rule. The dependent result classifier is unchanged by substitution composition. ◻

This corollary is preservation for the frozen beta fragment. It does not assert normalization or decidability for Idris 2, whose elaborator, effects, pattern compilation, and run-time system have a larger signature.

Zero demand is not proof irrelevance

Let $n{:}^0\mathsf{Nat}$ occur in the type $\mathsf{Vec}(A,n)$. The zero annotation says that evaluating the term does not inspect the run-time representation of $n$. The type checker may still distinguish $\mathsf{Vec}(A,0)$ from $\mathsf{Vec}(A,1)$, and a proof of $0=1$ is not thereby created.

Proof of Proposition 99.8 — Zero-context boundary

Proof. This is lemma 99.3. ◻

No operational erasure map has been defined, so the proposition makes no claim about compiled representations. It also gives neither proof irrelevance nor term equality: the closed terms $\mathsf{true}$ and $\mathsf{false}$ require no input resources but remain distinguishable by the Boolean eliminator.

Now consider an append operation The indices $n,m$ are checked and may occur repeatedly in the result type, but the program traverses the two vector values. In the Idris 2 v0.8.0 tutorial, the corresponding hole context prints $0$ beside $n$, $m$, and $A$, and no quantity beside the unrestricted vector arguments. That surface trace witnesses the implementation’s elaborated multiplicities; it is not the proof of theorem 99.6.

The pinned v0.8.0 transcript records the accepted elaboration state as

Main> :t append_rhs
 0 m : Nat
 0 a : Type
 0 n : Nat
   ys : Vect m a
   xs : Vect n a
-------------------------------------
append_rhs : Vect (plus n m) a

and the nearby attempted linear duplicator is rejected with

While processing right hand side of Main.duplicate:
There are 2 uses of linear name x

These are implementation observations from the retained tutorial [Idr26], not premises of the QTT proofs.

A nearby rejected definition has type $(x{:}^{1}A)\to (y{:}^{1}A)\otimes A$ and body $(x,x)$. Pair formation adds the two uses, producing demand $1+1$, not the binder’s promised $1$. An accepted linear state transition instead consumes a door once and returns the new door state, threading the result into the next operation.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 99.5, then complete exercise 99.7.

Exercise 99.5¶

★★☆ Reconstruct the QTT-App and QTT-Let cases of quantitative substitution over the natural-number semiring. Annotate each distributivity or associativity step and check the zero-output side conditions separately.

Referenced from 4 locations

• Quantitative Dependent Type Theory
• ch:quantitative-dependent-types: quantitative dependent type theory

Exercise 99.6¶

★★★ Use the zero–one–many semiring to reconstruct the failed substitution from the source calculus with an arbitrary output quantity. Exhibit the equation $\omega =1+\omega$, the premise derivation that would have to split, and the missing subusage rule. Then show why restricting output quantities to zero and one blocks the construction.

Referenced from 3 locations

• Quantitative Dependent Type Theory
• ch:quantitative-dependent-types: quantitative dependent type theory

Exercise 99.7¶

★★★ Practical project.qtt-demand-calculator Implement in Agda or Kappa context vectors over the natural-number and zero–one–many semirings, together with addition, scaling, and the application instance of quantitative substitution. Maintain the invariant that every output vector has the same declaration spine as its inputs. On the named cases twice-of-two, erased-index, and the promise-versus-inferred duplicate-use case, require these exact stdout fragments:

twice-of-two demand 4
erased-index demand 0
promise-vs-inferred rejects: promised 1, inferred many

Also require acceptance of a preserved $V_X,V_Y$ spine and rejection of a mismatched $V_X,V_Z$ spine. A mutation that makes spine comparison constantly true must fail the mismatch oracle. The calculator checks finite semiring equations; it does not prove admissibility for all QTT derivations or an Idris erasure theorem.

Referenced from 5 locations

• Quantitative Dependent Type Theory
• Rewriting and dependent resource systems: executable records
• ch:quantitative-dependent-types: demand calculation