Linear Dependent Type Theory

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

A dependent type may inspect its argument more than once. A linear term, however, must use a linear argument exactly once. Combining these two clauses naively makes the type checker consume a run-time resource: if $q:\mathsf{Qubit}$ and a type contains $B(q,q)$, then ordinary dependent substitution duplicates $q$. Declaring the two occurrences “static” does not repair the rule, because evaluating a general term in order to form a type may itself change the state.

The repair separates a resource-bearing value from the parameter that records its reusable shape. Types depend only on parameters; terms may still use state exactly once. The distinction is enforced by the judgments, not by an informal promise that the type checker will avoid dangerous evaluations.

Parameters and state

The indices form the three-element usage algebra used in the source calculus. Zero is the additive identity, one is the multiplicative identity, $k+\ell =\omega$ when $k,\ell \ne 0$, and $0k=0$, $\omega \omega =\omega$. Addition and scalar multiplication act pointwise on contexts with the same declaration spine. Consequently ${\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2$ is defined only when corresponding variables have the same types and its result is a well-formed context.

For example, a qubit has shape $\mathbf{1}$. A pair consisting of a natural parameter $n$ and an $n$-wire register retains $n$ but forgets the register state. Hence the shape may index a result type without giving the type checker permission to measure, copy, or discard the register.

The tempting replacement $\mathrm{Sh}(M)=M$ fails for state terms. If $M$ allocates or measures a qubit, putting $M$ into a type makes type formation stateful. The clause $\mathrm{Sh}(C)=\mathbf{1}$ is therefore load-bearing: it records that the state object exists while discarding the state itself.

The premise of LD-$⊸$-F exposes the separation. The term-level argument has type $A$, but the codomain receives only an argument of type $\mathrm{Sh}(A)$. No linear resource occurs in the kinding context.

Linear dependent functions and pairs

In LD-App, $N$ occurs once in the program and $\mathrm{Sh}(N)$ may occur repeatedly in the classifier. The two uses are not two resource uses. The same distinction appears in LD-Pair: $M$ contributes one state-bearing component, while its shape selects the second component’s type.

Take a base state type $\mathsf{Cell}$, a parameter type $\mathsf{Nat}$, and a family $\mathsf{Ready}:\mathsf{Nat}\to \ast$. Suppose $${\mathrm{\Gamma }}_f⊢f:(z:\mathsf{Cell})⊸\mathsf{Ready}(s@z)\text{and}{\mathrm{\Gamma }}_c⊢c:\mathsf{Cell},$$ where the codomain variable has type $\mathrm{Sh}(\mathsf{Cell})=\mathbf{1}$ and $s:\mathbf{1}\to \mathsf{Nat}$ is a parameter-level summary. Then LD-App derives $${\mathrm{\Gamma }}_f+{\mathrm{\Gamma }}_c⊢fc:\mathsf{Ready}(s@\mathrm{Sh}(c)).$$ The cell is consumed in $fc$; the reusable index is its unit-shaped summary. Since $\mathrm{Sh}(x)=x$ on variable syntax, the printed expressions $s@\mathrm{Sh}(c)$ and $s@c$ coincide after applying the meta-operation. Their typing role is nevertheless fixed: the occurrence of $c$ in the classifier has type $\mathrm{Sh}(\mathsf{Cell})=\mathbf{1}$, not $\mathsf{Cell}$.

Proof of Proposition 98.5 — Shape preservation

Proof. Induct on the typing derivation. In the variable case, applying shape to its declaration replaces the declared type by its parameter shape. For LD-App, the induction hypotheses give $$\mathrm{Sh}(M):(x:\mathrm{Sh}(A))\to \mathrm{Sh}(B[x])\text{and}\mathrm{Sh}(N):\mathrm{Sh}(A).$$ Parameter application therefore has the type on the left in $$\mathrm{Sh}(B)[\mathrm{Sh}(N)/x]=\mathrm{Sh}(B[\mathrm{Sh}(N)/x]),$$ where the equality follows by structural induction on $B$. The pair case uses the same commutation equation for the second component. Linear abstraction becomes parameter abstraction. Lift is fixed by shape, force becomes ${\mathsf{force}}^{\prime }$, and pair elimination commutes componentwise with shape. These cases cover every constructor in definition 98.1. ◻

Three substitutions

Ordinary substitution conflates three operations. A parameter may be put in a type, a parameter may be put in a term, and a state-bearing value may be put in a term while only its shape is put in dependent types. The theorem must state all three because the third induction invokes the first two.

Proof of Theorem 98.6 — Substitution

Proof. Prove the three clauses simultaneously by induction on the kinding and typing derivations. Parameter variables give clauses (1) and (2) by the usual variable split. Formation of either dependent linear former uses clause (1) under its parameter binder.

For clause (3), the variable case exposes the quantitative invariant. If the last rule selects $x$, then $k=1$ and the conclusion is precisely the given derivation ${\mathrm{\Gamma }}_2⊢V:A$, weakened by the zero-use declarations on either side. If it selects another variable, the declaration for $x$ has index zero in that branch; the induction conclusion adds $0{\mathrm{\Gamma }}_2$, so no resource in $V$ is consumed.

In the application case, split the premise occurrence of $x{:}_{k}A$ as $x{:}_{k_1}A+x{:}_{k_2}A$, where $k=k_1+k_2$. The two induction hypotheses produce contexts ${\mathrm{\Delta }}_1+k_1{\mathrm{\Gamma }}_2$ and ${\mathrm{\Delta }}_2+k_2{\mathrm{\Gamma }}_2$. Rebuilding LD-App is licensed by $$({\mathrm{\Delta }}_1+k_1{\mathrm{\Gamma }}_2)+({\mathrm{\Delta }}_2+k_2{\mathrm{\Gamma }}_2)={\mathrm{\Delta }}_1+{\mathrm{\Delta }}_2+(k_1+k_2){\mathrm{\Gamma }}_2.$$ Its result type is correct because shape commutes with value substitution: $$\mathrm{Sh}(N[V/x])=\mathrm{Sh}(N)[\mathrm{Sh}(V)/x].$$ The pair case has the same context equation, and the displayed shape equation aligns the second component’s type.

For linear abstraction, alpha-rename its binder away from $V$, apply the induction hypothesis under the binder, and rebuild LD-Lam. If the binder has index zero or $\omega$, its parameter-type side condition is unchanged by substitution. Pair elimination splits $k$ among the scrutinee and body and uses associativity and distributivity of context addition exactly as the application case. Lift has a parameter context, so a state-bearing substituted value can occur there only with scalar zero; force preserves the induction context. Parameter abstraction, parameter application, and ${\mathsf{force}}^{\prime }$ use clauses (1) and (2). Thus every formation and typing rule is rebuilt with the stated context. ◻

The value premise in clause (3) cannot be dropped for this call-by-value calculus. Substituting an arbitrary effectful computation duplicates or reorders its state transition when the variable occurs in a value body. The shape in the dependent suffix is equally necessary: replacing it by $V$ would insert a state term into a kinding judgment.

Evaluation and semantic soundness

Proof of Lemma 98.8 — Evaluation commutes with shape

Proof. Induct on the evaluation derivation. Application becomes parameter application, and the three induction hypotheses rebuild its evaluation rule. Pair elimination commutes with shape and with both substitutions. Force becomes ${\mathsf{force}}^{\prime }$, whose evaluation rule returns the shaped lifted body. Values are fixed by their corresponding parameter-value rules. These are all rules in definition 98.7. ◻

Proof of Proposition 98.9 — Preservation for evaluation

Proof. Induct on the evaluation derivation. In the application case, inversion of LD-App gives $${\mathrm{\Gamma }}_1⊢M:(x:B)⊸A[x],{\mathrm{\Gamma }}_2⊢N:B,\mathrm{\Gamma }={\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2.$$ The first two induction hypotheses type $\lambda x.M^{\prime }$ and $V$ at those same types. Inversion of LD-Lam and the fragment boundary give ${\mathrm{\Gamma }}_1,x{:}_{1}B⊢M^{\prime }:A[x]$. Apply theorem 98.6(3) to obtain $\mathrm{\Gamma }⊢M^{\prime }[V/x]:A[\mathrm{Sh}(V)/x]$. By lemma 98.8, $\mathrm{Sh}(N)\Downarrow \mathrm{Sh}(V)$; rule LD-ConvEval aligns this with $A[\mathrm{Sh}(N)/x]$, since the shaped value evaluates to itself. The final induction hypothesis types the result. Pair elimination uses the two successive instances of the same substitution clause. The force and parameter-application cases use their corresponding substitution clauses. Values close the induction. ◻

The restriction is load-bearing. The unrestricted source syntax permits LD-Lam with $k=0$ or $k=\omega$ when the domain is a parameter type, whereas LD-App always contributes one copy of the argument context. The published application proof explicitly supposes $k=1$ [FKS22]. Consequently the present chapter does not claim operational preservation for the other two cases without an additional parameter-weakening or parameter-substitution rule that aligns the required contexts.

Proof of Theorem 98.11 — Imported interpretation package

Proof. This is the exact import of clauses (1)–(7) of source Theorem 3.11. The hypotheses of definition 98.10 match Definition 2.8 clause for clause; the source’s simultaneous induction supplies the five groups above and the displayed context equation. No normalization, canonicity, or completeness conclusion is imported. ◻

Proof of Lemma 98.12 — Imported semantic value substitution

Proof. The imported result is the source’s value-substitution proposition [FKS22]. Its source diagram defines the arrow by the pullback universal property and defines the displayed arrow with precisely the domain printed above. This is the $k=1$, empty-suffix specialization; no undefined $\omega$-fold tensoring operation is used. ◻

Proof of Theorem 98.13 — Soundness for LD^1

Proof. Induct on the evaluation derivation. The application case contains the decisive step; its premises are $F\Downarrow \lambda x.M_0$, $N\Downarrow V$, and $M_0[V/x]\Downarrow W$. Typing inversion and proposition 98.9 give $${\mathrm{\Gamma }}_1,x{:}_{1}B⊢M_0:A[x],{\mathrm{\Gamma }}_2⊢V:B,\mathrm{\Gamma }={\mathrm{\Gamma }}_1+{\mathrm{\Gamma }}_2.$$ The three evaluation induction hypotheses give $$[[F]]=[[\lambda x.M_0]],[[N]]=[[V]],[[M_0[V/x]]]=[[W]].$$ Application is interpreted by the counit $ϵ$. Semantic substitution and the counit equation therefore yield the annotated chain The middle equality is exactly lemma 98.12; its source object is $[[{\mathrm{\Gamma }}_1]]\otimes [[{\mathrm{\Gamma }}_2]]$, so no implicit contraction duplicates $V$.

For pair elimination, interpret pair formation by dependent tensor and use semantic substitution twice; the tensor beta equation gives the required composite. Force uses the counit of the linear exponential, parameter application uses ordinary dependent-function beta in $\mathcal{B}$, and the remaining evaluation rules use functoriality followed by their induction hypotheses. Thus every ${\mathrm{LD}}^1$ evaluation derivation preserves its denotation. ◻

Dropping the state–parameter structure leaves the conclusion without a meaning: the application proof uses both the context-tensor equation and the dependent counit. Dropping the evaluation premise also fails; two terms of the same type need not denote the same morphism. Conversely, the theorem does not prove that evaluation terminates or that every closed value is canonical. The source states an unrestricted soundness result as Theorem 3.12, but its displayed application argument explicitly assumes $k=1$. The theorem above records the fragment established by that argument rather than silently generalizing it.

A resource-indexed protocol

Let $\mathsf{VecCell}(n)$ be the state type of a register containing exactly $n$ cells and let $\mathsf{Fin}(n)$ be the parameter type of valid positions. Consider $$\mathsf{read}:(n:\mathsf{Nat})\to (r:\mathsf{VecCell}(n))⊸(i:\mathsf{Fin}(n))\to \mathsf{Bit}\otimes \mathsf{VecCell}(n).$$ The parameter $n$ may be reused to check $i$, while the register $r$ occurs once. For $n=2$, $i=1$, and $r:\mathsf{VecCell}(2)$, the typing calculation is The first application consumes $r$; parameter application reuses $2$. An attempted second call with the same $r$ has context usage $1+1=\omega$, which is forbidden for the state type $\mathsf{VecCell}(2)$. The returned register, rather than the consumed name, must be threaded into the next call.

This protocol resembles an ownership API and its parameter index resembles a session-state index. Those resemblances do not identify the calculi: the present soundness proof depends on a state–parameter fibration and does not establish progress for a session operational semantics or borrowing laws for an ownership language.

The pinned Proto-Quipper-D tutorial exercises the same boundary in three stages [FKRS20]. Its first circuit boxes a reusable generator at type $$\mathsf{Circ}(\mathbf{1},\mathsf{Qubit}\otimes \mathsf{Qubit}),$$ separating the parameter-level circuit description from the state-bearing qubit wires. Its dependent Fourier-transform family then has the inspectable interface $$\mathsf{qftBox}:(n:\mathsf{Nat})\to \mathsf{Circ}(\mathsf{Vec}\mathsf{Qubit}n,\mathsf{Vec}\mathsf{Qubit}n).$$ The retained results bell00Box.pdf, teleBox.pdf, and qft5.pdf display the generated circuits; the vector length remains a parameter while each circuit consumes and returns its wire bundle.

The dynamic-lifting test measures a freshly initialized qubit, lifts the resulting bit into a host Boolean, and branches in a recursive binary-number calculation. A neighboring negative test attempts to use that dynamically lifted number as the length of a returned vector and is rejected: a run-time measurement cannot retroactively determine the static family in the result type. This implementation trace illustrates the state/parameter boundary; it is not a premise of theorem 98.13.

Suggested first pass.

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

Exercise 98.6¶

★★☆ Reconstruct all three clauses of theorem 98.6 for the term $(M,N)$. Identify the clause used for the second component’s type and the clause used for each component term. Test the boundary obtained by replacing $\mathrm{Sh}(V)$ with $V$.

Referenced from 4 locations

• Linear Dependent Type Theory
• ch:linear-dependent-types: linear dependent type theory

Exercise 98.7¶

★★★ For the application fragment, instantiate a state–parameter model whose parameter category is finite sets and whose state morphisms carry a finite state transition. Define the dependent counit and verify the semantic substitution square on a two-state example. State which additional structure would be required for pairs and $!A$.

Referenced from 3 locations

• Linear Dependent Type Theory
• ch:linear-dependent-types: linear dependent type theory

Exercise 98.8¶

★★★ Practical project.ldtt-shape-usage-checker Implement in Agda or Kappa the finite syntax consisting of state and parameter variables, linear application, dependent pairs, and shape. Maintain the invariant that a state variable has total usage at most one and that every classifier contains only parameter syntax. On the named threaded-read, duplicate-read, and raw-state-index inputs, require these exact stdout fragments:

threaded-read term accepted
duplicate-read term rejected for state usage
raw state index rejected during kinding

Also print the shape-substituted result type of threaded-read. The checker is a finite executable instance of the substitution invariant; it does not prove theorem 98.13.

Referenced from 5 locations

• Linear Dependent Type Theory
• Rewriting and dependent resource systems: executable records
• ch:linear-dependent-types: shape and usage checking