Chapter 186Optional

Linear-Dependent Quantum Programming and Proto-Quipper-D

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

Example 185.6 generated a circuit whose size is selected by a classical number, and the type of the result was $Circ (α, α)$ for every value of that number. That is correct and useless for the next step. Consider instead a circuit acting on $n$ wires — an adder on an $n$ -qubit register, or a Fourier transform of width $n$ . Its input interface has $n$ wires, so its type must mention $n$ : $qft : (n : Nat) \to Circ ({Qubit}^{n}, {Qubit}^{n}) .$ No type of definition 185.1 has this shape. The grammar of simple types is $T, U ::= α ∣ I ∣ T \otimes U$ , generated without reference to terms; a type ${Qubit}^{n}$ with $n$ a program variable is not in it, and adding it is not a matter of notation. Writing the family as a function $Nat \to Circ (T, U)$ for fixed $T, U$ fixes the width before $n$ is known; writing it as a list of circuits abandons the interface entirely, since $list Circ (T, U)$ still has one $T$ .

What is needed is a type former whose result depends on a term, together with a guarantee that evaluating a type never disturbs a quantum state. Both are supplied by making the dependency parametric: only terms with no effect on the quantum register may appear in types, and every term has a shape — its effect-free skeleton — which is what the type system actually substitutes. This chapter fixes that system, states its substitution and preservation theorems at their exact hypotheses, and builds the size-indexed family that chapter 185 could not type.

Signature delta

	Proto-Quipper-M	This chapter
Types	no dependency on terms; simple types generated from wire constants	dependent linear $Π$ and $Σ$ , with a separate parameter $Π$
Contexts	parameter context $Φ$ and label context $Q$ , kept apart	one context with usage indices $0, 1, ω$ ; a parameter context is one in which every linear type has index $0$
Duplication	$! A$ with $A$ a type; labels never duplicable	$! A$ , and additionally the index $ω$ permitted only at parameter types
Types and terms	disjoint	terms may occur in types, but only parameter terms, and a value is substituted into a type through its shape $Sh (V)$
Theorems used	theorem 185.9 (safety, soundness, adequacy)	none of them: the theorems of this chapter are proved for its own system (theorem 186.5, theorem 186.6)

The last row is the important one. Proto-Quipper-M’s adequacy does not transfer: its statement quantifies over its own configurations and its own category of labelled circuits, and the system below changes both the judgment form and the class of types. Chapter 40 supplies the general linear-dependent judgment and the separation of parameters from state; this chapter uses that vocabulary and proves its own metatheory.

The system

Definition 186.1 — Syntax ¶

Let $C$ range over base types of states, among them $Qubit$ . The grammars are $\begin{aligned} Types A, B ::= & C ∣ Unit ∣! A ∣ (x : A) ⊸ B [x] \\ ∣ & (x : A) \otimes B [x] ∣ (x : P_{1}) \to P_{2} [x], \\ Parameter types P ::= & Unit ∣! A ∣ (x : P_{1}) \otimes P_{2} [x] \\ ∣ & (x : P_{1}) \to P_{2} [x], \\ Terms M, N ::= & unit ∣ x ∣ λ x . M ∣ M N \\ ∣ & force M ∣ {force}_{0} R ∣ lift M \\ ∣ & (M, N) ∣ let (x, y) = N in M ∣ λ_{0} x . R ∣ R_{1} @ R_{2}, \\ Values V ::= & unit ∣ x ∣ λ x . M ∣ λ_{0} x . R ∣ lift M, \end{aligned}$ where the parameter terms $R$ are the terms built without $λ x . M$ , $M N$ , $force$ , and the state constants. Usage indices are $k ::= 0 ∣ 1 ∣ ω$ , and a context is a list $x :^{k} A$ in which $k = ω$ occurs only at a parameter type. A parameter context $Φ$ is a context in which every linear type has index $0$ . Addition and multiplication of indices are commutative with units $0$ and $1$ , with $k + ℓ = ω$ for $k, ℓ \neq 0$ , with $0 \cdot k = 0$ and $ω \cdot ω = ω$ , extended to contexts pointwise: $Γ_{1} + Γ_{2}$ adds indices and $k Γ$ multiplies them.

Referenced from 6 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Only parameter terms appear in types. The reason is operational and is worth stating before the rules: type checking evaluates the terms occurring in types, and if those terms could act on the quantum register, then type checking would change the state being described.

Definition 186.2 — Shape ¶

The shape operation maps types to parameter types and terms to parameter terms: $\begin{aligned} Sh (C) & = Unit, & Sh (! A) & =! A, & Sh (P) & = P, \\ Sh ((x : A) ⊸ B [x]) & = (x : Sh (A)) \to Sh (B [x]), \\ Sh ((x : A) \otimes B [x]) & = (x : Sh (A)) \otimes Sh (B [x]), \end{aligned}$ and on terms by $Sh (x) = x$ , $Sh (unit) = unit$ , $Sh (λ x . N) = λ_{0} x . Sh (N)$ , $Sh (M N) = Sh (M) @ Sh (N)$ , $Sh (force M) = {force}_{0} Sh (M)$ , $Sh (lift M) = lift M$ , componentwise on pairs and $let$ , and the identity on parameter terms. It is extended to contexts by applying it to every type.

Referenced from 7 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

The clause $Sh (C) = Unit$ is the whole idea: a state type has exactly one shape, so a wire contributes nothing to the type-level data, while its presence and count do, through the structure of the type. The operation is idempotent, and it is a meta-operation like substitution, not a term former.

Definition 186.3 — Selected typing rules ¶

Judgments are $Γ ⊢ M : A$ , with kinding $Φ ⊢ A : *$ and well-formed contexts $Γ ⊢$ . The rules that carry the dependency are $\frac{Γ ⊢ Sh (Γ) ⊢ A : * k = ω only if A is a parameter type}{Γ, x :^{k} A ⊢},$ $\frac{Φ, x :^{k} Sh (A) ⊢ B [x] : *}{Φ ⊢ (x : A) ⊸ B [x] : *}, \frac{Γ, x :^{1} A ⊢ M : B [x]}{Γ ⊢ λ x . M : (x : A) ⊸ B [x]},$ $\frac{Γ_{1} ⊢ M : (x : A) ⊸ B [x] Γ_{2} ⊢ V : A}{Γ_{1} + Γ_{2} ⊢ M V : B [Sh (V)]}, \frac{Φ ⊢ M : A}{Φ ⊢ lift M :! A},$ together with the rules for $\otimes$ , for the parameter arrow $\to$ with its $λ_{0}$ and $@$ , and for $force$ and ${force}_{0}$ . Every context appearing in a rule is required to be well formed, which is where the side condition on $ω$ is enforced.

Referenced from 5 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

The application rule shows the mechanism. The result type is $B$ with the shape of the argument substituted, not the argument: a value of a linear type may not appear in a type, but its shape may, and the shape carries exactly the information that survives erasing the state.

Substitution and preservation

Theorem 186.4 — Shape preserves typing ¶

If $Γ ⊢ M : A$ then $Sh (Γ) ⊢ A : *$ and $Γ ⊢$ ; moreover $Sh (Γ) ⊢ Sh (M) : Sh (A)$ .

Referenced from 5 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Proof of Theorem 186.4 — Shape preserves typing

Proof. Induction on the derivation of $Γ ⊢ M : A$ . At a variable, the context rule already contains the kinding premise, and $Sh (x) = x$ with the type replaced by its shape. At an abstraction, the induction hypothesis gives $Sh (Γ), x :^{k} Sh (A) ⊢ Sh (M) : Sh (B)$ , and the parameter abstraction rule concludes $Sh (Γ) ⊢ λ_{0} x . Sh (M) : (x : Sh (A)) \to Sh (B)$ , which is $Sh ((x : A) ⊸ B)$ by definition 186.2. At an application, the induction hypotheses give parameter terms of the corresponding parameter types and the rule for $@$ applies; the two shapes agree because $Sh$ is idempotent, so $Sh (B [Sh (V)]) = Sh (B) [Sh (V)]$ . The remaining constructors are formal copies of these three, with $Sh$ pushed through the constructor by the corresponding clause of definition 186.2. ◻

Theorem 186.5 — Substitution ¶

If $Φ, x : P, Φ^{'} ⊢ B [x] : *$ and $Φ ⊢ R : P$ , then $Φ, Φ^{'} [R / x] ⊢ B [R] : *$ .
If $Φ, x : P, Γ ⊢ M : B [x]$ and $Φ ⊢ R : P$ , then $Φ, Γ [R / x] ⊢ M [R / x] : B [R]$ .
Let $Γ_{1}, x :^{k} A, Γ^{'} ⊢ M : B [x]$ and $Γ_{2} ⊢ V : A$ . Then $Γ_{1} + k Γ_{2}, Γ^{'} [Sh (V) / x] ⊢ M [V / x] : B [Sh (V)] .$

Referenced from 10 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Proof of Theorem 186.5 — Substitution

Proof. Clauses (i) and (ii) are proved by simultaneous induction on the kinding and typing derivations. The substituted term $R$ is a parameter term, so it may be duplicated and may enter a type; the only case that is not a direct application of the induction hypothesis is the context rule, where the premise $Sh (Γ) ⊢ A : *$ becomes $Sh (Γ [R / x]) ⊢ A [R / x] : *$ by (i) applied at a smaller derivation, using that $Sh$ commutes with substitution of a parameter term because $Sh (R) = R$ .

Clause (iii) is the one whose statement is not the expected one, so its mechanism is written out. The term $V$ is a value, possibly of a linear type; it may therefore not be substituted into a type, and the statement substitutes $Sh (V)$ there instead. Consider the application case: $M = M_{1} V_{1}$ with $Γ_{1}^{'}, x :^{k_{1}} A ⊢ M_{1} : (y : A_{1}) ⊸ B_{1} [y]$ and $Γ_{1}^{″}, x :^{k_{2}} A ⊢ V_{1} : A_{1}$ , where $k = k_{1} + k_{2}$ and $Γ_{1} = Γ_{1}^{'} + Γ_{1}^{″}$ . The induction hypothesis applies to each premise with its own index, giving $Γ_{1}^{'} + k_{1} Γ_{2} ⊢ M_{1} [V / x]$ and $Γ_{1}^{″} + k_{2} Γ_{2} ⊢ V_{1} [V / x]$ , and the application rule concludes at the type $B_{1} [Sh (V_{1} [V / x])]$ . It remains to check that this is $(B_{1} [Sh (V_{1})]) [V / x]$ with $Sh (V)$ substituted for $x$ ; that is the equation $Sh (V_{1} [V / x]) = Sh (V_{1}) [Sh (V) / x]$ , which holds by induction on $V_{1}$ from definition 186.2, every clause of which commutes with substitution. Finally $(k_{1} + k_{2}) Γ_{2} = k_{1} Γ_{2} + k_{2} Γ_{2}$ by the arithmetic of indices, so the two contexts add to $Γ_{1} + k Γ_{2}$ . The abstraction and pair cases are the same argument with one and with two premises respectively; the variable case is the axiom together with $k = 1$ . ◻

Theorem 186.6 — Type preservation ¶

If $Γ ⊢ M : A$ and $M ⇓ M^{'}$ in the big-step call-by-value semantics, then $Γ ⊢ M^{'} : A$ .

Referenced from 6 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Proof of Theorem 186.6 — Type preservation

Proof. Rule induction on $M ⇓ M^{'}$ . The value rules are immediate. For application, $M = M_{1} M_{2}$ with $M_{1} ⇓ λ x . N$ , $M_{2} ⇓ V$ , and $N [V / x] ⇓ M^{'}$ ; the induction hypothesis gives $Γ_{1} ⊢ λ x . N : (x : A_{1}) ⊸ B [x]$ and $Γ_{2} ⊢ V : A_{1}$ , inversion of the abstraction rule gives $Γ_{1}, x :^{1} A_{1} ⊢ N : B [x]$ , and theorem 186.5(iii) with $k = 1$ gives $Γ_{1} + Γ_{2} ⊢ N [V / x] : B [Sh (V)]$ , which is the type assigned to $M$ by the application rule. A second use of the induction hypothesis transports this to $M^{'}$ . The cases for pairs, $let$ , $force$ , and the parameter constructs are formal copies, each using the clause of theorem 186.5 matching the sort of the substituted term. ◻

Theorem 186.4, Theorem 186.5, Theorem 186.6 are Theorem 3.6, Theorem 3.7, and Proposition 3.10 of Fu, Kishida, and Selinger, Linear Dependent Type Theory for Quantum Programming Languages [FKS22]; the proofs above follow their inductions and are written out here for the cases in which the shape operation does visible work. That paper additionally constructs a denotational interpretation in a state-parameter fibration and proves its soundness, its Theorems 3.11 and 3.12; those are not reproduced here, and no statement of this chapter depends on them.

A size-indexed circuit family

Definition 186.7 — Wire vectors ¶

Let $Nat$ be a parameter type with constructors $0$ and $succ$ , and define the family of state types $Vec Qubit 0 : = Unit, Vec Qubit (succ n) : = Qubit \otimes Vec Qubit n .$ Its shape is $Sh (Vec Qubit n) = Unit$ for every $n$ by definition 186.2, while the type itself depends on $n$ ; the index is a parameter and the wires are states.

Referenced from 2 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Example 186.8 — A chain of controlled gates ¶

Let $CNOT$ have type $! (Qubit \otimes Qubit ⊸ Qubit \otimes Qubit)$ . Define by recursion on the parameter $n$ $chain : (n : Nat) \to! (Qubit \otimes Vec Qubit n ⊸ Qubit \otimes Vec Qubit n)$ by $chain 0 : = lift (λ p . p)$ and $\begin{aligned} chain (succ m) : = lift (λ p . & let (c, v) = p in \\ let (w, v^{'}) = v in \\ let (c^{'}, w^{'}) = (force CNOT) (c, w) in \dots), \end{aligned}$ where the omitted part applies $force (chain m)$ to $(c^{'}, v^{'})$ and reassembles the result with $w^{'}$ . The recursion is on $n$ , which is a parameter and may therefore be inspected and used twice; the wires $c, w, v^{'}$ each occur exactly once, as the linear rules require.

Boxing gives $chainbox : (n : Nat) \to Circ (Qubit \otimes Vec Qubit n, Qubit \otimes Vec Qubit n)$ . For $n = 3$ the generated circuit has three $CNOT$ gates and the interface $(ℓ_{0} : Qubit, ℓ_{1}, ℓ_{2}, ℓ_{3} : Qubit) ⟶ (ℓ_{0}^{'}, ℓ_{1}^{'}, ℓ_{2}^{'}, ℓ_{3}^{'}),$ four wires in and four out, which is what the type says once $n$ is instantiated. Compare example 185.6: there the type was $Circ (α, α)$ for every $n$ , and the generated circuit’s interface was not visible in it.

Referenced from 4 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Example 186.9 — Type-safe uncomputation ¶

A circuit that computes a value while producing garbage has type $a ⊸ WithGarbage b$ , where the monad $WithGarbage$ records a vector of garbage wires together with its length; the operation $dispose$ adds one wire to that vector. Because the length is an index and not a constant, the number of garbage wires produced by a computation need not be known when the combinator below is typed.

The combinator takes a garbage-producing $f :! (a ⊸ WithGarbage b)$ and a consumer $g :! (c \otimes b ⊸ d \otimes b)$ and returns a garbage-free $c \otimes a ⊸ d \otimes a$ . It is built from an existential boxing operation whose type is $existsBox : (p : b \to Type) \to! (a ⊸ (n : b) \otimes p n) \to (n : b) \otimes Circ (a, p n),$ which boxes a circuit-generating function whose output interface is not known in advance, returning the width $n$ together with a circuit at that width. The combinator then unboxes the circuit, runs it, applies $g$ to the useful output, and applies the reverse of the same circuit to the garbage, which restores the input wires. Every step is typed: the two uses of the boxed circuit are at the same $n$ because $n$ is bound once by the $Σ$ -type, and the reverse has the interface exchanged.

The boundary is exactly stated by the authors of the system: the type guarantees that no garbage wire is left uncollected, and it does not guarantee that the uncomputed wires are returned in the state $| 0 ⟩$ . Semantic correctness of the generated circuit is not decided by the type system; a failure of it is a programming error and not a type error. This distinction is the same one drawn in remark 185.11, now applied to a construction whose types have become expressive enough to make the confusion tempting.

Referenced from 5 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Exercise 186.1 ¶

★☆☆ Compute $Sh (A)$ for $A = Qubit \otimes Vec Qubit n$ , for $A =! (Qubit ⊸ Qubit)$ , and for $A = (x : Nat) \to Circ (Qubit, Qubit)$ , and say in each case which information about $A$ survives.

Referenced from 2 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Exercise 186.2 ¶

★★☆ Let $Γ_{2} ⊢ V : Qubit$ . Using the index arithmetic of definition 186.1, compute $Γ_{1} + k Γ_{2}$ for $k = 0, 1, ω$ and say which of the three is excluded by well-formedness, and why.

Referenced from 2 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Exercise 186.3 ¶

★★☆ Explain why $(x : Qubit) \to P [x]$ is not a type of definition 186.1, and why $(x : Qubit) ⊸ B [x]$ is. Then show that the second is only useful when $B$ depends on $x$ through $Sh (x)$ , and compute what that dependency can be.

Referenced from 3 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Comparisons and boundary

A mechanized circuit language. QWIRE embeds a circuit language in Coq, where circuits are typed by an inductive family and their well-typedness is a Coq proposition; a development in it is checked by the host proof assistant. The comparison is instructive precisely at the trust boundary: in QWIRE the guarantee is “Coq accepted this proof about this embedded circuit”, with the embedding itself part of what must be trusted, whereas in the system above the guarantee is “this term has this type in the calculus of definition 186.3”, with the type checker part of what must be trusted. Neither statement implies the other, and neither implies semantic correctness of the circuit, by example 186.9.

Reversing and control. A modern Proto-Quipper variant adds a modality for reversible computations, a control operation, and a $with$ - $computed$ construct as a primitive rather than a derived combinator. As a rule delta against definition 186.3: types gain a modal former marking reversibility, the boxing rule gains a premise that the boxed function is reversible, and the reverse operation becomes a term former rather than a library function. Its own authors leave the combination of that modal system with the dependent types of this chapter open, so no theorem and no implementation is transferred here; what is transferred is the observation that $with$ - $computed$ can be primitive.

Dependent indices verify the stated interfaces. They do not verify amplitudes, they do not verify that a gate is implemented correctly by hardware, and they do not establish an algorithmic speedup. Example 186.8 guarantees that a circuit of width $n + 1$ is produced for input $n$ ; whether that circuit computes anything useful is a separate question with a separate proof.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 186.4, then exercise 186.5; the implementation project exercise 186.7 may be attempted at any time.

Exercise 186.4 ¶

★★☆ Construct two size-indexed circuit families: one applying $H$ to every wire of $Vec Qubit n$ , and one applying $CNOT$ to every adjacent pair. Give the type of each, compute the generated interface for $n = 3$ , and count the gates as a function of $n$ .

Referenced from 3 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Exercise 186.5 ¶

★★☆ Write out the pair case of theorem 186.5(iii) in full, including the index arithmetic and the shape equation $Sh (V_{1} [V / x]) = Sh (V_{1}) [Sh (V) / x] .$ Then exhibit a term for which substituting $V$ rather than $Sh (V)$ into the type produces a type that is not well kinded.

Referenced from 3 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Exercise 186.6 ¶

★★☆ Repair the following unsafe uncomputation attempt: a program applies $f$ to produce a result and garbage, applies $g$ , and then discards the garbage wires with $dispose$ instead of running the reverse circuit. State which type in example 186.9 rejects the attempt, and what physical difference the rejection corresponds to.

Referenced from 2 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Exercise 186.7 ¶

★★★ Practical project.indexed-circuit-checker Implement in Agda or Kappa a type checker and circuit generator for the fragment of definition 186.1, definition 186.3 containing $Unit$ , $Qubit$ , $! A$ , linear $⊸$ and $\otimes$ , the parameter arrow, $Nat$ with recursion, and the family $Vec Qubit n$ . Implement the shape operation, index arithmetic on contexts, kinding, typing, and generation of the circuit for a closed boxed term.

The invariant to maintain is the pair proved in theorem 186.4, theorem 186.5: every type is kinded in the shape of its context, and substituting a value into a type goes through $Sh$ . The concrete result is a function taking a closed term of type $(n : Nat) \to Circ (\dots)$ and a numeral, and returning the generated circuit with its input and output interfaces.

Acceptance test. For $chainbox$ of example 186.8 at $n \in {0, 1, 3}$ the tool reports circuits with $0$ , $1$ , and $3$ gates and interfaces of width $1$ , $2$ , and $4$ ; the term of exercise 186.3 using $(x : Qubit) \to P [x]$ is rejected at kinding, with the checker naming the parameter-type premise; a term that uses a wire variable twice is rejected by index arithmetic, with the checker printing the offending index $ω$ at a non-parameter type; and substituting a value into a type without applying $Sh$ — the prescribed mutation — must make the tool accept a term whose reported result type mentions a qubit variable, which the kinding check must then reject.

The program checks and generates finite circuits for closed terms at fixed numerals. It illustrates theorem 186.5, theorem 186.6 and proves neither, and it establishes nothing about the semantics of the generated circuit, in accordance with example 186.9.

Referenced from 3 locations

Linear-Dependent Quantum Programming and Proto-Quipper-D

Bibliographic notes

The syntax, shape operation, typing discipline with indices, substitution theorem, and type preservation of section 186.2, section 186.3 are those of Fu, Kishida, and Selinger, Linear Dependent Type Theory for Quantum Programming Languages [FKS22]: definition 186.1 is its Definition 3.1, definition 186.2 its Definition 3.2, theorem 186.4 its Theorem 3.6, theorem 186.5 its Theorem 3.7, and theorem 186.6 its Proposition 3.10. Its denotational interpretation in a state-parameter fibration and the corresponding soundness theorem are its Theorems 3.11 and 3.12 and are not used here. The general linear dependent judgment and the separation of parameters from state are developed in chapter 40.

The size-indexed families and the uncomputation combinator of section 186.4 follow the tutorial of Fu, Kishida, Ross, and Selinger [FKRS20], which contains the $WithGarbage$ monad, the $existsBox$ operation, and the $with$ - $computed$ combinator, together with the explicit statement that the system guarantees syntactic and not semantic correctness of the generated circuit; a pinned experimental implementation accompanies it. QWIRE is retained as an independent mechanized comparison, and the modal Proto-Quipper with reversing and control [FKRS26] as the bounded rule-and-example delta of section 186.5.