Substructural Type Systems

Most type systems let you do whatever you want with a value: use it once, use it ten times, or never use it at all. Substructural type systems restrict these freedoms — and it turns out that restricting what you can do with a value is one of the most powerful ideas in programming language design.

The Four Flavors

A substructural type system controls two properties of values: whether you can duplicate them (use more than once, called "contraction") and whether you can discard them (use fewer than once, called "weakening"). The four combinations give you four kinds of types:¹

• Unrestricted: use any number of times. This is the default in most languages.
• Affine: use at most once. You can throw it away, but you can't duplicate it.
• Relevant: use at least once. You must use it, but you can duplicate it.
• Linear: use exactly once. No duplication, no discarding.

The names come from substructural logic — specifically, from removing structural rules (contraction and weakening) from the sequent calculus. By the Curry-Howard correspondence, every logic gives rise to a type system. Classical logic gives unrestricted types. Remove contraction and you get relevant types. Remove weakening and you get affine types. Remove both and you get linear types.²

The naming is a mess, and Aria Beingessner (who literally wrote the book on unsafe Rust) marks the standard terminology with a "Trademark of Disdain" because people constantly confuse the variants. When someone says they want "linear types in Rust," they almost always mean they want better support for relevant types — must-use values — not actual linear types, which would be far more restrictive.¹

Rust's Affine Core

Rust's ownership system is the most commercially successful substructural type system in existence. At its heart, Rust uses affine types — what Rust calls "move semantics." When you pass a value by value, the original binding is consumed. You can't use it again:

let x = vec![1, 2, 3];
let y = x;           // x is moved
println!("{:?}", x); // ERROR: use of moved value

A "use" in Rust's model is specifically a pass-by-value operation. Pass-by-reference doesn't count as a use, because the borrow checker ensures all references are gone before any real use happens. This is the key insight: affine types give you a simple way to prove you have unique access to a value. If you hold an affine value by-value, you know nobody else can see it. That makes it safe to do destructive operations like freeing memory.¹

This model also enables elegant protocol enforcement. If step1() returns a token that step2() consumes, and step2() returns a token that step3() consumes, then the type system guarantees the steps happen in order and none are repeated:

let t1 = step1();
let t2 = step2(t1);
step3(t2);
step2(t1); // ERROR: use of moved value

The borrow checker layers on top of this with rules about shared (&T) versus exclusive (&mut T) references. This is where Rust's aliasing model comes in: &mut T is guaranteed to be the only live reference to the value, which means the compiler can optimize based on non-aliasing assumptions and the programmer can mutate without fear of data races. The distinction between shared-immutable and exclusive-mutable references isn't just a safety feature — it's an aliasing discipline that enables the kind of optimizations C compilers have to guess at.³

The Missing Piece: Must-Use Types

The one thing Rust's move semantics can't enforce is that you actually do something with a value. Affine types prevent double-use but permit discard. You can make sure step2 happens after step1, but you can't force step2 to happen at all.

Rust has some partial answers. The unused_variables lint catches obvious cases. The #[must_use] annotation warns when a return value is ignored. And Drop provides a destructor that runs when a value goes out of scope — a kind of "guaranteed final step." But Drop has real limitations: it can't return a value, it can't take extra parameters, and there's only one of it per type.¹

For truly must-use semantics — relevant types — Beingessner sketches what full support would require: a Leave trait (analogous to Copy for duplication) that controls whether a value can be discarded, with a ?Leave bound for generic code that opts into must-use values. The sketch is technically feasible but painful: it would require auditing and upgrading the entire standard library, adding ?Leave bounds everywhere, and dealing with the interaction between must-use values and panicking (a panic can prevent a must-use value from being consumed). It's "a lot of paper cuts that pile up to make an overall unpleasant system."¹

The panic problem deserves special mention. If any function can panic, and panicking unwinds the stack, then a must-use value might be dropped without being properly consumed. The solutions are either a no-panic effect system (infectious and burdensome) or making all must-use types abort on panic (depressing but practical). This is a microcosm of a general truth about substructural types: they compose poorly with effects.

The ABI Question

There's a practical dimension to type system design that theorists sometimes overlook: how does your type system interact with dynamic linking? Swift and Rust make an illuminating comparison here.

Both languages use monomorphization — compiling generic code by copy-pasting it with concrete types substituted in. This is great for performance but hostile to dynamic linking, because a generic function has no single compiled form. C++ templates have the same problem, which is why the C++ standard library is famously unfriendly to dynamic linking.⁴

Swift solved this by making generics polymorphically compilable — generic code can be compiled to use value witness tables that describe how to copy, move, and destroy values at runtime. The tradeoff is overhead: every operation on a generic value requires an indirect call through a witness table. But it means Swift can ship its standard library as a single system-wide dylib, which Apple cares about intensely for iOS memory footprint.

Rust chose the other path. Monomorphization everywhere, no stable ABI, and if you want a dynamic interface you write a C-like extern boundary. The Rust team has largely embraced this: ABI stability is a means to the end of dynamic linking, and Rust has decided the cost of achieving it isn't worth the constraints it would impose on the type system's evolution.⁴

The Landscape

The deep insight connecting all of this is the one from the Curry-Howard correspondence: for every logic system, there's a type system, and vice versa. Affine logic gives you Rust's ownership. Linear logic gives you session types and protocol verification. Ordered logic (where you can't even reorder uses) gives you stack-based languages. Separation logic gives you fine-grained reasoning about heap-allocated data.

There are far more logics in the academic literature than type systems that have been implemented as real languages. Each one represents a different way of disciplining computation — a different set of invariants the compiler can check, a different class of bugs it can prevent. The history of programming languages has been a slow migration from "no type system" (assembly) through "weak types" (C) to "strong types" (ML, Haskell) to "substructural types" (Rust). The question is what comes next, and the answer is probably already sitting in a logic textbook somewhere, waiting for someone to build a compiler for it.