Linear Types

Linear types ensure resources are used exactly once. In Kettle, this is crucial for quantum computing where qubits cannot be copied.

Why Qubits?

In quantum computing, a qubit (quantum bit) is the fundamental unit of quantum information—analogous to a classical bit, but with different properties.

Unlike classical bits (which are always 0 or 1), a qubit can exist in a superposition of both states simultaneously. When you measure a qubit, it "collapses" to either 0 or 1, but until measurement, it holds both possibilities at once. This property enables quantum algorithms to explore many solutions in parallel.

Kettle's quantum features let you create and manipulate qubits, apply quantum gates (operations), and measure results. But qubits have a fundamental constraint that classical data doesn't: they cannot be copied.

The No-Cloning Theorem

The no-cloning theorem is a fundamental result in quantum mechanics: you cannot copy an arbitrary quantum state. This is a physical law, not just a programming limitation. The following code would violate physics:

-- This would be invalid!
fn bad_copy() -> Unit with Quantum
  q: Qubit = 0
  q <- hadamard
  copy1 = q  -- use q
  copy2 = q  -- use q again - ERROR!
end fn

Kettle's type system catches this at compile time.

Linear Values

A linear value must be used exactly once:

• Cannot be used zero times — no dropping/ignoring
• Cannot be used more than once — no copying

Qubits are linear:

fn valid() -> Int with Quantum
  q: Qubit = 0       -- create qubit
  q <- hadamard      -- use it (rebind)
  measure(q)         -- consume it
end fn

Creating Qubits

Create qubits using type-directed construction with Qubit = 0 (for |0>) or Qubit = 1 (for |1>). For multiple qubits, use List[Qubit] = [0, 0, ...]:

Initial State

Using Qubit = 0 creates a qubit in |0>, and Qubit = 1 creates one in |1>:

The qubit() and qubits(n) functions are also available for dynamic use cases, but prefer the type-directed syntax in new code.

Using Linear Values

Rebinding

Transform a linear value with <-:

fn apply_gates() -> Int with Quantum
  q: Qubit = 0
  q <- hadamard      -- q is rebound
  q <- pauli_x       -- q is rebound again
  measure(q)         -- q is consumed
end fn

Passing to Functions

Functions consume linear arguments:

fn measure(q: Qubit) -> Int with Quantum
  -- q is consumed here
end fn

fn use_qubit() -> Int with Quantum
  q: Qubit = 0
  measure(q)  -- q is passed and consumed
  -- can't use q here anymore
end fn

Returning Linear Values

Functions can return linear values:

fn prepare_plus() -> Qubit with Quantum
  q: Qubit = 0
  q <- hadamard
  q  -- return the qubit
end fn

fn main() -> Int with Quantum
  q = prepare_plus()  -- receive the qubit
  measure(q)          -- must eventually consume it
end fn

Discarding Linear Values

Sometimes you need to consume a qubit without using its measurement result. Use discard():

The discard() function consumes the qubit, satisfying linearity requirements. This is useful when you only care about some qubits in a computation.

Tuples of Linear Values

You can group linear values in tuples:

fn bell() -> Tuple[Qubit, Qubit] with Quantum
  -- creates and returns two entangled qubits
end fn

fn use_bell_pair() -> Tuple[Int, Int] with Quantum
  (a, b) = bell()           -- destructure
  (measure(a), measure(b))  -- consume both
end fn

Common Patterns

Process and Measure

fn process(q: Qubit) -> Int with Quantum
  q <- hadamard
  q <- pauli_z
  measure(q)
end fn

Thread Through Circuit

fn circuit() -> Int with Quantum
  q: Qubit = 0
  q <- hadamard
  q <- pauli_x
  q <- hadamard
  measure(q)
end fn

Multi-Qubit Operations

fn entangle_and_measure() -> Tuple[Int, Int] with Quantum
  q1: Qubit = 0
  q2: Qubit = 0

  q1 <- hadamard
  q1, q2 <- cnot  -- two-qubit gate, rebinds both

  (measure(q1), measure(q2))
end fn

Compiler Errors

The compiler prevents common mistakes:

Using a Value Twice

Forgetting to Use

fn forget() -> Unit with Quantum
  q: Qubit = 0
  -- Error: q is never used (leaked)
end fn

Branching Issues

fn branch_problem(cond: Bool) -> Unit with Quantum
  q: Qubit = 0
  match cond
    True -> measure(q)
    False -> ()  -- Error: q not consumed in this branch
  end match
end fn

The fix—consume in all branches:

fn branch_fixed(cond: Bool) -> Int with Quantum
  q: Qubit = 0
  match cond
    True -> measure(q)
    False -> measure(q)  -- consumed in both branches
  end match
end fn

User-Defined Linear Types

You can define your own linear types with the linear keyword:

linear type FileHandle = record
  fd: Int
  path: String
end record

linear type DatabaseConnection = record
  conn_id: Int
  host: String
end record

These types follow the same rules as Qubit—must be used exactly once:

fn open_file(path: String) -> FileHandle with IO
  -- allocate a file handle
  FileHandle(fd = 1, path = path)
end fn

fn close_file(handle: FileHandle) -> Unit with IO
  -- handle is consumed here
  ()
end fn

fn use_file() -> Unit with IO
  handle = open_file("data.txt")
  -- ... use handle ...
  close_file(handle)  -- must be consumed
end fn

Linearity Propagates Through Containers

If a generic type contains a linear value, the whole container becomes linear:

type Box[T] = record value: T end record

-- Box[Qubit] is linear because it contains a Qubit
fn box_example() -> Int with Quantum
  q: Qubit = 0
  b = Box[Qubit](q)        -- b is linear (positional construction)
  q = b.value              -- extracting consumes b
  measure(q)
end fn

Non-Linear Types

Most types in Kettle are not linear—they can be used freely:

fn normal_code() -> Unit with IO
  x = 42
  y = x + 1  -- use x
  z = x + 2  -- use x again - fine!
  print(to_string(x))  -- and again
end fn

Only types marked as linear (like Qubit) have usage restrictions.

Why Linear Types?

Linear types provide:

1. Safety — Impossible to write quantum code that violates physics
2. Resource management — Resources are always properly cleaned up
3. Optimization — Compiler knows values won't be aliased

The restrictions might seem limiting, but they prevent entire classes of bugs and make quantum code reliable.

Next Steps

• Gates — Applying quantum operations to qubits
• Effects System — How effects and linearity interact