Questions: Linear Types

Question 1

A value with a linear type must be used exactly once. What does 'used' mean in this context?

• A. The value must appear exactly once in the source code text
• B. The value must be consumed by exactly one operation at runtime — it cannot be passed to two different functions (duplication) or ignored without being consumed (discarding)
• C. The value must be of a primitive type
• D. The value must be immutable

Answer: (B)

Linear usage means the value is consumed exactly once along every execution path. If you have a linear file handle, you must eventually close it (consume it) — not closing it is a type error (discard). You cannot pass it to two functions that both try to close it (duplication). The type system tracks this statically, ensuring that resources are managed correctly regardless of which branches or loops execute.

Question 2

Rust's ownership system is based on affine types, not strictly linear types. What is the difference?

Model answer: Affine types allow values to be used AT MOST once (can be discarded but not duplicated), while linear types require values to be used EXACTLY once (no discarding, no duplication). Rust is affine: you can let an owned value go out of scope without explicitly consuming it (the destructor runs automatically). A strictly linear system would require explicit consumption, making it harder to use in practice.

The distinction matters for resource management. In a linear system, a file handle MUST be explicitly closed — the type system forces you to call close(). In Rust's affine system, the handle is closed when dropped (by the destructor), which happens automatically at scope exit. This is more ergonomic while still preventing duplication (which would cause double-close bugs). Rust adds borrowing on top of affine ownership to allow temporary shared access without consuming the value.

Question 3

How do linear types prevent data races in concurrent programs?

Model answer: If a mutable value has a linear type, it can be owned by exactly one thread at a time — the type system prevents two threads from simultaneously holding a reference to the same mutable data. To share data between threads, you must explicitly transfer ownership (consuming the value in the sender and creating it in the receiver) or use a synchronization primitive. Since data races require two threads accessing the same memory with at least one writing, and linear types prevent shared mutable access, data races are ruled out by construction.

This is the insight behind Rust's concurrency safety guarantees ('fearless concurrency'). The borrow checker ensures that mutable references are unique (at most one &mut T) and shared references are immutable (multiple &T, no mutation). This is a form of affine discipline applied to references: a mutable reference is used linearly (exactly one owner), preventing concurrent mutation. The safety guarantee is static — no runtime overhead, no data race possible in safe Rust.

Question 4

Linear types are connected to Girard's linear logic through the Curry-Howard correspondence.

• T. True
• F. False

Answer: True

Just as the Curry-Howard correspondence connects intuitionistic logic to simply-typed lambda calculus, it connects linear logic to linear type theory. In linear logic, hypotheses must be used exactly once — you cannot reuse a premise without the explicit 'of course' modality (!A). Under Curry-Howard, this translates to: values of linear type must be consumed exactly once, and values that can be freely copied require a special 'unrestricted' (non-linear) type. This logical foundation gives linear type systems their clean theoretical properties.