Rust Inference Rules for Linear Types

Rust does not have a formal, published set of inference rules in the same way as languages designed around formal type systems (like those in type theory literature). However, it enforces linearity (or more accurately, affine types, which are a relaxation of linear types) using a combination of:

• Move semantics

• Borrow checking

• Lifetime inference

• Ownership rules

That said, we can reconstruct the effective inference rules Rust uses for linearity from the compiler’s behavior. Below is a breakdown of these inference-style rules as they relate to linear/affine types in Rust.

🔁 Ownership and Affine Type Rules (Rust Core Inference)

In Rust, most types are affine, meaning a value may be used at most once (but may be dropped without use).

1. Move Rule

If x: T is a move type, and used in a move context, then x is consumed and cannot be used again.

Rust will infer that a value has been moved if it is passed by value or assigned to another variable:

let x = String::from("hello");
let y = x; // move occurs
// x is now invalid

⛔ use of moved value: x

2. Copy Rule

If T: Copy, then values of type T can be duplicated freely.

let x = 5;
let y = x; // copy, not move
// x is still valid

3. Borrow Rule

If x: T, then &x: &T and &mut x: &mut T may be created, respecting aliasing rules.

This is the core of affine resource tracking. Rust’s borrow checker enforces:

• At most one mutable reference, or

• Any number of shared references, but not both

let mut x = 42;
let r1 = &x;
let r2 = &x; // ok: multiple shared
// let r3 = &mut x; // error: can't borrow mutably while shared refs exist

4. Return Ownership

A function that returns a value must transfer ownership or borrow it.

fn take(v: Vec<i32>) -> Vec<i32> {
    v // move back to caller
}

5. Drop Rule

If x: T goes out of scope and T: Drop, then drop(x) is implicitly called.

If you don’t use a value before the end of the scope, it is dropped exactly once. This is part of affine behavior: no duplication and no leaks.

6. Destructuring Rule

When a struct/tuple is destructured, each part is moved (or borrowed), unless it implements Copy.

let (a, b) = (String::from("hi"), String::from("bye"));

// a and b are both moved

7. Pattern Matching Move/Borrow Inference

In a match or if let, the type determines whether fields are moved or borrowed.

if let Some(s) = x {
    // s is moved, x is no longer valid
}

But:

let x = Some(String::from("hi"));

if let Some(ref s) = x {
    // s is a reference, x is still valid
}

🧠 Lifetime and Borrow Inference Rules

Rust also infers lifetimes for borrowed values, which interact with linear usage:

8. Lifetime Elision Rules (subset)

fn foo(x: &T) -> &T

// becomes
fn foo<'a>(x: &'a T) -> &'a T

These rules help the compiler ensure borrowed references don’t outlive the data they point to — critical for affine guarantees.

🔂 Loop and Branch Rules for Linear Values

If you introduce a linear value in a loop or branch, it must be used in all paths.

let x = String::from("hi");
if cond {
    drop(x);
} else {
    drop(x); // must also use x here
}

🧪 Function Signature-Based Inference

9. Function Parameters Move by Default

fn consume(s: String) { ... } // s is moved into the function

Unless T: Copy or the argument is a reference.

10. Closure Inference

move || { ... } captures variables by value (moves them)

|| { ... } captures by reference

The compiler infers capture mode based on what the closure does:

• Uses it by move → infers move

• Uses it immutably → infers Fn

• Mutably → FnMut

• Consumes → FnOnce

🧩 Not Quite Linear: Rust is Affine

A linear type must be used exactly once.

Rust’s types are affine: they must be used at most once. You are allowed to not use a value — Rust will just call drop.

fn f(x: String) {
    // ok to do nothing: x is dropped
}