Linear Type Systems · Quantum PL Wiki

A linear type system treats a binding as a resource that must be used exactly once along each execution path. Ownership can be transferred, transformed, or explicitly consumed. Quantum languages use such disciplines to prevent unrestricted duplication of qubit resources. This supports the physical distinction between quantum information and copyable classical records described in quantum states and operations.

Linearity concerns a program's resource usage. It does not mean that a physical qubit may undergo only one gate: an operation may return a new binding through which the same evolving resource remains available.

A resource-sensitive example

In an illustrative linear interface, the types of a Hadamard gate and a destructive measurement are

H:\mathrm{Qubit}\multimap\mathrm{Qubit}, \qquad \mathrm{measure}:\mathrm{Qubit}\multimap\mathrm{Bit}.

The linear arrow indicates that the input resource is consumed by the call. A small program could read:

let q1 = h q
let b = measure q1
return (b, b)

The original binding q is unavailable after h q; q1 is unavailable after measurement. Duplicating b is allowed if Bit is unrestricted. Attempting let pair = (q, q) would use the same linear binding twice and be rejected.

Measurement need not destroy the physical qubit. A different interface may use $\mathrm{Qubit}\multimap(\mathrm{Bit}\otimes\mathrm{Qubit})$ , returning both the result and the post-measurement resource. The type must match the language's operational convention.

Contexts and physical meaning

A typing judgment often separates an unrestricted context $\Gamma$ from a linear context $\Delta$ : $\Gamma;\Delta\vdash e:A$ . Rules for combining independent expressions split $\Delta$ , preventing the same resource from being assigned to both expressions. Classical control may mention a resource in alternative branches, provided the typing rules ensure consistent usage on the branch actually executed.

A pair of qubit resources may be entangled; a tensor type does not assert a product quantum state. Discarding one subsystem is modeled by a partial trace, not by deleting its amplitudes from a state vector. Affine types allow at most one use; strictly linear languages may instead provide an explicit discard operation.

Limitations

Linearity can enforce ownership and usage constraints only when the type rules, primitives, and implementation are sound. It does not itself prove gate identities, output probabilities, termination, or algorithmic correctness. Nor does every quantum programming language adopt the same linear discipline.

This introductory interface is pseudocode, not a claim about a specific compiler. Higher-level specifications require additional verification methods.

References

P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. Computer Science Logic, 121-135 (1995). DOI: 10.1007/BFb0022251.
Peter Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527-586 (2004). DOI: 10.1017/S0960129504004256.