Quantum Type Theory

There is no single formalism universally called quantum type theory. Instead, typed quantum languages combine several ideas to solve one stable design problem: distinguish classical information from quantum data and prevent programs from expressing physically impossible operations.

The central themes are resources, effects, and reversible evolution. Linear typing tracks the ownership of quantum data; effect systems expose measurement and discard; circuit disciplines or stronger types guarantee that coherent evolution is physically valid.

Notation at a glance

Notation	Meaning
$A\multimap B$	A function that consumes one resource of type $A$ and produces a $B$
$A\otimes B$	A pair containing both an $A$ resource and a $B$ resource
$|\psi\rangle$	A quantum state (“ket psi”)
$U^\dagger$	The adjoint, or conjugate transpose, of $U$

A classical bit is definitely 0 or 1. A qubit can instead be in a superposition of the two basis states:

$$|\psi\rangle=\alpha|0\rangle+\beta|1\rangle,\qquad |\alpha|^2+|\beta|^2=1.$$

The complex numbers $\alpha$ and $\beta$ are amplitudes. Their squared magnitudes are probabilities, so they must add to one. An isolated quantum system evolves by a unitary transformation which is a reversible map that preserves this probability structure. A language must therefore respect two separate constraints:

1. An arbitrary unknown quantum state cannot be cloned.
2. Coherent evolution must preserve inner products, not merely use each input once.

The no-cloning theorem

There is no unitary operation clone satisfying

$$\operatorname{clone}(|\psi\rangle|0\rangle)=|\psi\rangle|\psi\rangle$$

for every unknown state $|\psi\rangle$. If a unitary cloned both $|\psi\rangle$ and $|\phi\rangle$, preservation of inner products would require

$$\langle\psi|\phi\rangle=\langle\psi|\phi\rangle^2.$$

The equation can hold only when the overlap is $0$ or $1$: the states are orthogonal or identical. It fails for arbitrary states, which proves that a universal quantum copier cannot exist. A CNOT gate can copy a known basis value, but it does not independently clone an arbitrary superposition (Wootters and Zurek 1982; Dieks 1982).

Ordinary variables behave like information written on a whiteboard: we can read them repeatedly. A qubit behaves more like a physical object checked out from a lab: the type checker must know who currently owns it. Many quantum languages express this by splitting the typing context:

$$\Gamma;\Delta\vdash e:A.$$

Context	Role	Structural behavior
$\Gamma$	Classical, unrestricted information	Values may be copied or ignored
$\Delta$	Linear quantum resources	Each resource must be accounted for

Read the judgment as: “using reusable assumptions $\Gamma$ and quantum resources $\Delta$, expression $e$ produces a value of type $A$.” Strictly linear systems require a variable exactly once. Affine systems permit use at most once; discarding is then allowed syntactically, but its semantics is an irreversible quantum operation (Selinger and Valiron 2006).

Why is the example rejected? Constructing a pair requires constructing both halves. The typing rule divides the available quantum resources between those two jobs:

$$\frac{\Gamma;\Delta_1\vdash e_1:A\qquad\Gamma;\Delta_2\vdash e_2:B}{\Gamma;\Delta_1,\Delta_2\vdash(e_1,e_2):A\otimes B}$$

The contexts $\Delta_1$ and $\Delta_2$ are disjoint. The single resource q can go to the left or right premise, but not both, so the attempted duplication cannot type-check.

Tensor elimination consumes the package

A tensor $A\otimes B$ is a package containing both resources. Ordinary projections such as fst could silently abandon one component, so a linear calculus normally opens the package by naming both:

$$\frac{\Gamma;\Delta_1\vdash e:A\otimes B\qquad\Gamma;\Delta_2,x:A,y:B\vdash f:C}{\Gamma;\Delta_1,\Delta_2\vdash\mathbf{let}\;(x,y)=e\;\mathbf{in}\;f:C}.$$

The first signature describes a gate acting on two existing qubits, conventionally initialized to $|00\rangle$. The second allocates fresh qubits. Allocation changes the visible collection of wires, so it belongs to an effectful interface rather than being a unitary map from “nothing.”

In a strictly linear calculus, measuring only one half of a fresh Bell pair leaves the other half unaccounted for and is rejected. The programmer must return, measure, reset, or explicitly discard the second qubit.

Measurement is where quantum data becomes ordinary classical information. It consumes a qubit and returns a reusable bit:

$$\frac{\Gamma;\Delta\vdash q:\mathrm{Qubit}\qquad\Gamma,b:\mathrm{Bit};\Delta'\vdash e:C}{\Gamma;\Delta,\Delta'\vdash\mathbf{let}\;b=\operatorname{measure}(q)\;\mathbf{in}\;e:C}$$

The rule has three important steps:

1. The qubit q is taken from the linear context.
2. Measurement consumes q and produces the classical bit b.
3. The continuation may reuse b because it enters $\Gamma$.

The simple function type hides a probabilistic effect: measuring $\alpha|0\rangle+\beta|1\rangle$ yields 0 with probability $|\alpha|^2$ and 1 with probability $|\beta|^2$.

Languages can represent this effect through probabilistic operational semantics, monads, effect types, or denotations by completely positive maps (Selinger 2004; Selinger and Valiron 2006).

Linearity is needed to avoid cloning and properly deal with quantum resources. But the other part of the puzzle is that the operations have to be unitary and something can be linear but not unitary.

A linear type controls how a program uses a resource. It says that the input qubit must be consumed exactly once; it does not say what physical operation is performed on that qubit.

Consider an effectful reset operation:

reset q consumes q exactly once and returns a qubit initialized to $|0\rangle$. It therefore obeys the ownership rule expressed by $\multimap$. However, an input in state $|0\rangle$ and an input in state $|1\rangle$ produce the same visible result. The original state information has been lost, so the operation cannot be reversed.

A unitary operation describes closed, reversible quantum evolution. It must preserve all information about its input, which is expressed by

$$U^\dagger U=UU^\dagger=I.$$

The type Qubit ⊸ Qubit proves only that the program accounts for one input and one output qubit. A separate circuit discipline, effect system, or stronger type is needed to prove that the operation is unitary.

How languages enforce valid evolution

1. Unitary primitives and closure rules. Build circuits from trusted gates, known to be unitary, using sequential composition, tensor product, wire permutation, control, and adjoint.
2. Separate reversible and effectful fragments. Track whether a circuit is reversible or controllable while isolating initialization, measurement, reset, and discard (Fu et al. 2024).
3. Orthogonality and normalization checks. Verify that distinct basis inputs map to orthogonal, normalized outputs. QML and realizability-based systems pursue this approach (Altenkirch and Grattage 2005; Díaz-Caro et al. 2019, 2023).

Circuit sizes often depend on classical parameters. Dependent types can express families of registers and circuit generators:

For example, setting n = 5 produces a circuit whose output register has type QVec 5. The number is known while the circuit is generated; the five qubits exist only when that circuit runs. The Unit argument distinguishes a reusable circuit description from its resource-producing execution.

Proto-Quipper-D uses linear dependent types to describe circuit families and verify properties such as garbage-free uncomputation (Fu et al. 2020). Its crucial distinction is:

• Parameters are available at circuit-generation time and may occur in types.
• State data exists only when the generated circuit executes.

A measurement result may control later runtime computation. With dynamic lifting, it can even become a parameter that guides generation of the next circuit segment, explicitly requiring interaction between the classical controller and quantum device (Fu et al. 2022).

Quantum teleportation transfers an unknown state using prior entanglement, two classical bits, and local operations. It neither clones the state nor communicates faster than light (Bennett et al. 1993).

Follow the resources line by line:

1. 1newBell creates entangled qubits a and b.
2. 2CNOT and H combine Alice's unknown qubit phi with her Bell-pair half a.
3. 3Two measurements consume Alice's qubits and produce reusable classical bits c1 and c2.
4. 4Those bits select a correction on Bob's qubit b, which becomes the single output qubit.

The original physical carrier of $|\phi\rangle$ has been measured. The protocol transfers the state without ever producing two independent copies.

It may seem that reversible gates cannot express ordinary irreversible computations. The trick is to keep enough information to run the computation backward. Toffoli gates are universal for classical reversible computation, and an irreversible Boolean function can be embedded as:

$$(x,y)\longmapsto(x,y\oplus f(x)).$$

The input is retained while the result accumulates in a target register. Erasing arbitrary information on the same closed register would violate reversibility; the information must instead remain as output, garbage, or environmental state.

Quantum Turing machines and uniform families of unitary circuits are standard universal models (Deutsch 1985; Bernstein and Vazirani 1997). Intermediate measurement is convenient but not generally required: deferred measurement can replace many measurements and classically controlled gates with coherent controls followed by final measurement.

BQP stands for Bounded-Error Quantum Polynomial Time. It contains decision problems for which a uniform quantum algorithm:

• runs in polynomial time, and
• returns the correct yes/no answer with probability at least $2/3$ on every input.

The threshold $2/3$ is conventional. Repeating the computation and taking a majority vote can make the error exponentially small without leaving polynomial time.

$$\mathrm{P}\subseteq\mathrm{BPP}\subseteq\mathrm{BQP}\subseteq\mathrm{PP}\subseteq\mathrm{PSPACE}.$$

Read each $\subseteq$ as “every problem in the class on the left is also in the class on the right.” None of the potentially strict inclusions displayed above is known to be strict. Shor gave polynomial-time bounded-error quantum algorithms for integer factoring and discrete logarithms (Shor 1997). Thus factoring is in BQP, but it is not known whether factoring is in P (although many expect it is not).

• Altenkirch, Thorsten, and Jonathan Grattage. 2005. “A Functional Quantum Programming Language.” LICS 2005. arXiv:quant-ph/0409065.
• Bennett, Charles H., et al. 1993. “Teleporting an Unknown Quantum State via Dual Classical and Einstein-Podolsky-Rosen Channels.” Physical Review Letters 70: 1895–1899. doi:10.1103/PhysRevLett.70.1895.
• Bernstein, Ethan, and Umesh Vazirani. 1997. “Quantum Complexity Theory.” SIAM Journal on Computing 26: 1411–1473. doi:10.1137/S0097539796300921.
• Deutsch, David. 1985. “Quantum Theory, the Church–Turing Principle and the Universal Quantum Computer.” Proceedings of the Royal Society A 400: 97–117. doi:10.1098/rspa.1985.0070.
• Díaz-Caro, Alejandro, et al. 2019. “Realizability in the Unitary Sphere.” LICS 2019. arXiv:1904.08785.
• Díaz-Caro, Alejandro, et al. 2023. “A Feasible and Unitary Quantum Programming Language.” arXiv:2311.01054.
• Dieks, Dennis. 1982. “Communication by EPR Devices.” Physics Letters A 92: 271–272. doi:10.1016/0375-9601(82)90084-6.
• Fu, Peng, et al. 2020. “A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper.” arXiv:2005.08396.
• Fu, Peng, et al. 2022. “Proto-Quipper with Dynamic Lifting.” arXiv:2204.13041.
• Fu, Peng, et al. 2024. “Proto-Quipper with Reversing and Control.” arXiv:2410.22261.
• Selinger, Peter. 2004. “Towards a Quantum Programming Language.” Mathematical Structures in Computer Science 14: 527–586. doi:10.1017/S0960129504004256.
• Selinger, Peter, and Benoît Valiron. 2006. “A Lambda Calculus for Quantum Computation with Classical Control.” Mathematical Structures in Computer Science 16: 527–552. arXiv:cs/0404056.
• Shor, Peter W. 1997. “Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer.” SIAM Journal on Computing 26: 1484–1509. doi:10.1137/S0097539795293172.
• Wootters, William K., and Wojciech H. Zurek. 1982. “A Single Quantum Cannot Be Cloned.” Nature 299: 802–803. doi:10.1038/299802a0.