Qubits and registers

A circuit type tells you how many qubits flow through, but it says nothing about the qubits themselves as values. In Quon a qubit is a first-class value with a linear type, and the way you group qubits into registers — and reshape those registers — is deliberately constrained. This page introduces the two qubit-bearing types and the operations that change a register’s shape, and explains why Quon refuses to let you index into a register the way a classical array would.

Qubit and QReg<n>

A Qubit is a single linear quantum value: one qubit, owned exactly once, consumed exactly once. A QReg<n> is a single linear value that bundles a statically known number n of qubits. The n is a compile-time Nat, so QReg<2> and QReg<3> are distinct types — you cannot accidentally pass a three-qubit register where a two-qubit register is expected. Both Qubit and QReg live in the linear context, which means every qubit they contain must be accounted for before it goes out of scope.

The distinction matters because of how composition works. A Circuit<n, m, ...> applied to a QReg<n> consumes the whole register and produces a QReg<m>; the register is the unit of application. But many algorithms need to reach individual qubits — to apply a gate to one and not its neighbor, or to pair a qubit from one register with a qubit from another. Quon does not let you reach into a register by index. Instead it forces you to destructure the register into named qubits, making ownership explicit at every step.

QReg in run blocks

Registers are created inside run blocks by the qreg(n) allocator, which produces a fresh QReg<n> of n qubits all in |0⟩. A circuit is then applied to the register with the @ operator, consuming it and producing a new register (or a tuple of individual qubits if the circuit’s output width is split):

fn prepare_and_split(): Q<(Qubit, Qubit)> = run {
    reg <- bell_state() @ qreg(2)
    let (q0, q1) = destructure(reg)
    return (q0, q1)
}

Here qreg(2) allocates the register, bell_state() @ qreg(2) applies the circuit (consuming the QReg<2> and producing a new QReg<2>), and destructure splits that output register into two named qubits. The circuit application is the bridge between the typed circuit value and the monadic world: it is the only way a circuit touches live qubits.

Destructuring and reshaping

destructure takes a QReg<n> and splits it into n individual Qubit values, each of which you bind to a name. Once destructured, the qubits are independent linear values you can reorder, recombine, or feed to circuits one at a time. To put qubits back together — say, to reverse a pair — you re-tensor them into a new register:

fn reverse_pair(q: QReg<2>): QReg<2> =
    let (left, right) = destructure(q)
    in (right, left)

Here destructure(q) yields the two qubits as left and right; the expression (right, left) tensors them back into a QReg<2> in reversed order. Two further operations complete the reshaping toolkit. split(k, reg) divides a register into its first k qubits and the remaining tail, returning both as separate registers. tensored combines two registers (or qubits) into one wider register. Together these let you change a register’s shape — split it, reorder pieces, join pieces from different sources — while preserving linear ownership at every step.

split: extracting a prefix

split(k, reg) is the operation you reach for when an algorithm needs only part of a register — for instance, the data qubit out of a decoded block, leaving the syndrome qubits for cleanup. It returns a pair (QReg<k>, QReg<n - k>):

fn take_first(q: QReg<5>): (QReg<2>, QReg<3>) =
    let (head, tail) = split(2, q)
    in (head, tail)

The split point k is a compile-time Nat, so the result types are statically known. You cannot split a QReg<2> at position 5 — the typechecker rejects it because 5 > 2.

tensored: joining registers

tensored (also written as tuple formation (a, b)) combines two registers — or a register and a bare qubit, or two bare qubits — into one wider register. This is how you assemble a multi-qubit register from parts:

fn join_up(a: Qubit, b: QReg<2>): QReg<3> = (a, b)

The total width is the sum of the parts. The operation consumes both inputs and produces a single linear value — there is no aliasing, because the original names are gone from the linear context after the join.

Reordering by destructuring

A common pattern is to destructure a register, permute the qubits, and re-tensor them into a new register with a different wire order. This is how you reverse wires in a QFT, or swap which qubit is the control in a two-qubit gate:

fn swap_wires(q: QReg<2>): QReg<2> =
    let (a, b) = destructure(q)
    in (b, a)

fn rotate_three(q: QReg<3>): QReg<3> =
    let (a, b, c) = destructure(q)
    in (c, a, b)

Every qubit is accounted for by name at every step. The typechecker tracks each one through the linear context: destructure removes the register and introduces the individual qubits, and the tuple formation re-introduces a single register. No qubit is lost, no qubit is duplicated.

Why no indexing

A natural question: why not just write reg[1] to grab the second qubit? The answer is aliasing. In a classical array, reg[1] is a reference into storage that the array still owns; you can read it, copy it, and the array is unchanged. A qubit cannot be copied (no-cloning), and a “reference” to a qubit that someone else still holds would be a second name for the same linear resource — exactly the ambiguity that breaks linearity. If two names could reach the same qubit, the typechecker could no longer guarantee single use.

Quon closes that hole by making destructure, split, and tensored the only way to change a register’s shape, and by having each of them move ownership rather than alias it. When you destructure a register, the original register is consumed and ceases to exist; the qubits now live only under their new names. There is no way to hold the register and an element of it at the same time. This keeps the linear context simple — a QReg<n> is always one linear value, never a bag of individually borrowable aliases — and it keeps the no-cloning guarantee a local, checkable fact rather than a global hope.

What goes wrong without the restriction

Consider what a hypothetical reg[i] operation would have to mean. It would produce a Qubit while leaving reg intact — so the same qubit would have two names in the linear context, and the typechecker could not enforce single use. You could then pass both names to two different gates, effectively cloning the qubit’s state, which the no-cloning theorem forbids. By forcing destructuring to consume the register, Quon makes this error a structural impossibility: after destructure(reg), the name reg is unbound, so there is nothing left to index into.

Splitting in practice

A common pattern is to encode one logical qubit into several physical ones, operate, then decode back to one. Decoding leaves a multi-qubit register from which you want only the first qubit; split extracts it while carrying the remainder (here ignored with _) along for cleanup:

fn bit_flip_round(logical: Qubit): Q<QReg<1>> = run {
    encoded        <- (encode()) @ logical
    (data, s1, s2) <- syndrome_measure(encoded)
    corrected      <- correct(data, s1, s2)
    decoded        <- adjoint(encode()) @ corrected
    let (out, _rest) = split(1, decoded)
    return out
}

Don’t worry about the run block, measure, or adjoint yet — those belong to later pages. Notice the shape: encode widens one qubit into a register, syndrome_measure and correct work on the register as a whole, adjoint decodes it back, and split(1, decoded) pulls out the single logical qubit as out while _rest names the auxiliary qubits for discard. Every qubit is accounted for by name; nothing is indexed, nothing is aliased.

Register width mismatch errors

Because QReg<n> carries n in the type, a width mismatch between a circuit’s expected input and the register you supply is a type error, not a runtime check. The typechecker compares the circuit’s n against the register’s n and rejects mismatches before the elaborator runs:

fn bad_apply(): Q<QReg<2>> = run {
    out <- bell_state() @ qreg(3)
    return out
}

error: width mismatch in circuit application
  --> source.qn:2:14
   |
 2 |     out <- bell_state() @ qreg(3)
   |              ^^^^^^^^^^^    ^^^^^^^
   |              Circuit expects 2 input qubits, register has 3
   |
   = hint: use split(2, qreg(3)) to take the first 2 qubits

The diagnostic points at both the circuit and the register, naming the conflicting widths and offering a fix. This is the typechecker doing the work the compiler reference calls “width discharge” — a refinement obligation discharged by structural equality of the Nat arguments, without needing Z3.

Interaction with circuit application

Circuit application — the @ operator — is where register types meet circuit types. The operator has the typing rule:

c : Circuit<n, m, d, C>    reg : QReg<n>
------------------------------------------ @
        c @ reg : Q<QReg<m>>

The input register is consumed (removed from the linear context) and a fresh output register is produced. If the circuit is not square (n ≠ m), the output register has a different width than the input — encode takes a QReg<1> and produces a QReg<3>, decode reverses it. The typechecker proves the width transformation at every application site, so you can chain circuits of different widths knowing the interfaces will line up.

When the output width is small, you can destructure immediately:

fn bell_prepare(): Q<(Qubit, Qubit)> = run {
    (q0, q1) <- bell_state() @ qreg(2)
    return (q0, q1)
}

Here bell_state() @ qreg(2) produces a QReg<2>, and the pattern (q0, q1) destructures it in the same binding. The typechecker verifies that the circuit’s output width (2) matches the pattern’s arity (2) — a width mismatch here is the same kind of error as the qreg mismatch above.

For the normative form of qubit and register types — syntax, typing contract, constraints, and a minimal valid example — see the Language reference.

Next

You have now seen that qubits are linear values consumed exactly once — but we have only asserted that. The next page makes the linear type system precise: the linear context, what “consume” really means, which values are unrestricted, and the shape of the type errors you get when the rules are broken.

→ The linear type system