The Linear Types / Rust Ownership Connection — oversimplification or legit?

You've already answered your own question, but let me lay out the taxonomy formally because I see people get this wrong constantly.

The key table looks like this:

──────────────────┬───────────┬──────────────┬────────────────
                  │ WEAKENING?│ CONTRACTION? │ USES
──────────────────┼───────────┼──────────────┼────────────────
Normal types      │    YES    │     YES      │ Any number
Affine types      │    YES    │              │ At most once
Relevant types    │           │     YES      │ At least once
Linear types      │           │              │ Exactly once
──────────────────┴───────────┴──────────────┴────────────────

In current Rust, all types have the law of weakening, but by default types do not have the law of contraction.

"Weakening" means you can discard a value without using it (drop). "Contraction" means you can copy/duplicate it. Rust allows weakening (via Drop) but not contraction (unless you implement Copy). That's affine, not linear.

What Rust is not able to express is a coin type that cannot go out of scope — that would take a linear type. Under the resource interpretation, a linear type not only can be moved, like an affine type, but must be moved — going out of scope is an invalid program.

Historically though the connection isn't just a blog-post shortcut. The concept of linear types is inspired by linear logic, a substructural logic introduced by Jean-Yves Girard in 1987. And Rust's design draws from that lineage — it's not an accident or coincidence.

There's an academic paper on a formal model of Rust called Oxide that makes this explicit: the system draws ideas from linear and ownership types, citing Girard 1987. Yet Rust goes beyond prior art in developing a particular typing discipline that aims to balance both expressivity and usability, so Rust has something interesting to teach us about making ownership practical for programming.

So yes: Rust is affine, not linear. But it's affine in a way that is directly descended from the linear logic tradition. It's not a coincidence; it's an intentional design choice to relax linearity for practical reasons.

MOD NOTE Great thread, keeping it open. Let me add the academic angle.

The "substructural" framing is the right one here. Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances. Such systems can constrain access to system resources such as files, locks, and memory by keeping track of changes of state and prohibiting invalid states.

Rust's ownership is specifically affine because of the Drop trait. Rust may have affine types, but it currently doesn't have types which cannot be weakened — that is, types which must be used at least once. There's a lot of interest in specifically linear types, types which must be used exactly once. This term has been misused by some contributors to the Rust project to refer to a different idea around leaks, but it has also been used to refer to adding proper linear types to the language, which have also been called "must move" types or "undroppable" types.

The "must move" / "undroppable type" idea is what would make it truly linear. We don't have that in stable Rust today.

Right, and there's actually a workaround some crates use in practice: one extreme option is to implement drop() as abort("this value must be used"). All "proper" consumers then mem::forget the value, preventing this "destructor bomb" from going off. This provides a dynamic version of strict must-use values. Although it's still vulnerable to the few ways destructors can leak, this isn't a significant concern in practice — mostly it just stinks because it's dynamic and Rust users Want Static Verification.

The "destructor bomb" pattern. I've seen it in some protocol state-machine crates. It's clever but it's not the same as a compile-time linear type guarantee.

The practical motivation behind all of this is worth emphasizing for people coming from a PL theory background who haven't done much systems programming. One particular resource that has been shown to be a good match for linear (and affine) type systems is memory. Programming languages can use linear types to get the "best of both worlds" between memory-safe, garbage-collected languages like Java and "memory-unsafe" languages like C and C++ that use manual memory management.

This is exactly what Rust is doing — linear types (and the general area of substructural type systems, of which linear types are one example) have recently influenced a cadre of safe programming languages with manual memory management: most prominently, Rust, which was in turn influenced by Cornell's Cyclone language.

Cyclone → Rust. If you want to understand the intellectual lineage properly, read about Cyclone first.

Lurker here. What does this mean for borrowing? The whole &T / &mut T system seems to break the "use at most once" story?

Rust defines a "use" to be pass-by-value. Pass-by-reference isn't considered a use, because we want a way to actually make use of these values more than once. The borrow checker makes sure we get rid of all these references before we perform a "real" use.

So does borrowing "break" the affine property? Asking genuinely.

Good question. Short answer: no, borrowing is carefully carved out. Uses that don't transfer ownership — borrowing — are not in scope of this interpretation, but lifetime semantics further restrict these uses to be between allocation and deallocation. Under the resource interpretation, an affine type cannot be spent more than once.

Longer answer: there's recent formal work on this. Borrowing generalises the concept of ownership, permitting multiple references to point to a single value simultaneously. Rust's borrow checker manages all borrows that exist at a given time, ensuring that memory safety properties are maintained until values are eventually returned to their owners.

The formal relationship between ownership, uniqueness types, and linear types is actually more nuanced than it might appear. There's recent OOPSLA work showing that ownership can be better understood as an extension of uniqueness types, since each value having a single owner implies that the owner holds the unique reference to said value.

To bring in GHC as a comparison: Haskell actually has proper linear types now via -XLinearTypes (shipped in GHC 9.0). The approach taken there is quite different from Rust's.

In GHC Linear Types, a function f is linear if: when its result is consumed exactly once, then its argument is consumed exactly once. Intuitively, it means that in every branch of the definition of f, its argument x must be used exactly once.

They encode this via multiplicity on function arrows: there is a new function type a %m -> b. Here, m is a type of new kind Multiplicity. We have data Multiplicity = One | Many, where One is the linear arrow and Many is the regular arrow.

So GHC's approach is a function-level constraint. Rust's approach is more of a value/type-level constraint. These are different engineering choices for realizing related formal ideas.

This is a good observation and worth expanding. The linear-base library shows what you can do with real linear types in Haskell: the library exports new abstractions that leverage linear types for resource safety or performance — including new APIs for file and socket I/O as well as for safe in-place mutation of arrays.

There's also a cool non-GC memory angle: you can use linear types to enforce the protocols for using memory outside of GHC's garbage collector and on the system heap — that we allocate before use, necessarily free, and do not use after that. Hence the GC has less work to do.

So Linear Haskell is converging on the same problems Rust was solving but from a completely different starting point (lazy FP vs systems programming). Very interesting to see them meeting in the middle.

What about session types? I see this cited in connection with linear types a lot. Does Rust help here?

The easiest way to explain how linear types are useful is to talk about session types. The idea of session types is to encode the protocol of some concurrently executing process in the type system so that you can only perform operations which are legal based on the state that concurrent process is in.

Linear types prevent the problem of dropping a session type because you must use the session type. You can use the session type by calling commit or abort, or you can use it by moving it to a new function.

Rust's affine system gets you part of the way there (you can use token-passing state machines) but not fully, because you can still drop the token without "completing" the protocol. The destructor bomb pattern mentioned earlier is one workaround, but it's runtime rather than compile-time.

Another angle I want to bring up: Baker's Linear Lisp. People always cite Girard but the direct influence on Rust is arguably more from Baker's work on 'use-once' variables.

From the Oxide paper: Rust's ownership model is best understood as instead building off of Baker's work on Linear Lisp where linearity enabled efficient reuse of objects in memory. The resemblance is especially strong between Rust without borrowing and Baker's 'use-once' variables.

And importantly: Rust's main departure from techniques like 'use-once' variables is a softening — i.e. borrowing is exactly that softening. The borrow checker is the mechanism that lets you temporarily violate the use-once property without losing its safety guarantees.

The "use-once" token pattern in Rust is genuinely powerful even if it's not "true" linear types. Here's a simple illustration of typestate encoding:

// Token-passing typestate — affine style
fn step1() -> Step1Token;  // open/connect/init
fn step2(Step1Token) -> Step2Token;  // write/send
fn step3(Step2Token);  // close/free/destroy

// The compiler prevents calling step2 before step1,
// or calling step1 twice. Protocol violation = compile error.

More broadly, this system can be used as a proof of work. If you need step1() to always precede step2(), you can use a move-only value to enforce this. What you can't prevent is someone just dropping the token mid-protocol without a compile error. That's the gap.

OK so I went and read the without.boats ownership post (great blog btw). The Rc / destructor leaking thing is the key problem:

Rust chose to allow reference counted pointers which do no cycle breaking, so every guarantee based on destructors has to be caveated with the fact that destructors maybe don't run. There has been interest in changing this so that you can define a type which can't be leaked ("unforgettable types"), which then can't be put into a shared ownership construct safely.

So even the "destructor bomb" pattern isn't 100% safe — you can leak a bomb into an Rc cycle and it never detonates. That's a compelling argument that Rust is fundamentally affine and adding "real" linear types would require quite significant language changes.

Here's the real verdict: is saying "Rust has linear types" an oversimplification or outright wrong?

I'd say it's a category error if stated precisely, but a useful approximation in educational contexts. Here's why:

✅ The motivation is the same: resource control, preventing double-use, safe memory management.
✅ The intellectual lineage is real: Girard → Wadler → Cyclone → Rust.
✅ The structural rules analysis (contraction banned, weakening allowed) is correct type theory.
❌ But "linear" specifically means exactly once, and Rust types are at most once.
❌ And Rust's borrowing system is a significant departure from a naive linear type system.

Best description: "Rust has an affine type system derived from linear logic research." If you say "Rust has linear types" on a PL exam, expect to lose points.

What does the Clean language do here? I've seen it cited in discussions of uniqueness types.

The Clean programming language makes use of uniqueness types (a variant of linear types) to help support concurrency, input/output, and in-place update of arrays.

And linear logic is not just a valuable memory management strategy — it is also a valuable aliasing and data race strategy. Clean introduced uniqueness types in 1992 for IO handling and destructive updates. Later languages like ATS, Alms, and Mezzo explored this idea in different ways.

The Rust team specifically drew on this research: the Rust team was in touch with these teams and stayed abreast of a wealth of research underway at the same time. Rust's resulting ownership-based model is largely based on the mutual exclusion idea that one either has a single mutable reference to an object, or possibly-multiple immutable references to that object.

One more thing worth mentioning: recent formal work tries to unify all of this. One approach allows many ideas from Rust, such as immutable and mutable borrows, partial borrows and reborrowing, to be explained explicitly in a functional setting through the application of a form of grading based on fractional permissions. This work thus integrates and relates, within a unified framework, the substructural type systems of linearity, uniqueness, grading, ownership, and borrowing.

So the academic consensus is moving toward: ownership/borrowing and linearity are related but distinct concepts that can be unified under a more general framework of graded/resource types. Neither "Rust is linear types" nor "Rust has nothing to do with linear types" is quite right.

Recommended reading for this thread:

📄 Girard (1987) — "Linear Logic," Theoretical Computer Science 50(1):1–102. The source.
📄 Wadler (1990) — "Linear types can change the world" — accessible intro, great title.
📄 Weiss et al. (2019) — "Oxide: The Essence of Rust" — formal Rust semantics, free on arXiv.
📄 Bernardy et al. (2018) — "Linear Haskell" (POPL'18) — the paper behind -XLinearTypes.
📄 Marshall & Orchard (2024) — "Functional Ownership through Fractional Uniqueness" (OOPSLA'24) — the unification story.
🔗 CGPA megathread: Substructural Type Systems 101
🔗 GHC LinearTypes in practice — experiences & pitfalls

Also see affine types in other languages — there's a thread on how Cyclone, ATS, and Vale approach this.

And for the Haskell side: the purpose of linear-base is to provide the minimal facilities you need to write practical Linear Haskell code, i.e., Haskell code that uses the -XLinearTypes language extension. Worth experimenting with if you want to feel the difference between Rust-style affine and Haskell-style linear firsthand.

CONCLUSION Great thread everyone. Let me try to summarize the consensus:

1. Rust is technically an affine type system (use at most once), not a linear type system (use exactly once). Calling Rust "linear types" on a formal exam is incorrect.
2. The connection to Girard's linear logic and its tradition is real and substantial — Rust's design consciously draws from this lineage via Cyclone, Baker's Linear Lisp, uniqueness types, etc.
3. The key distinguishing feature Rust lacks: types that must be used (no weakening). GHC's -XLinearTypes gets closer to real linear types at the function-arrow level.
4. Borrowing is what makes Rust's system practical but also makes it significantly more complex than a naive affine type system — it's closer to fractional permissions + uniqueness types in recent formal treatments.
5. "Oversimplification or legit?" → Oversimplification, but a defensible one if you specify "affine" and acknowledge the borrow checker complexity.

Marking as [RESOLVED]. Ping me if I missed anything.