Linear Types

Superseded by RFC-0028 (Memory and Reference Model). This document is kept as historical record. All decisions and open questions have been carried forward into RFC-0028. Note: the read reference syntax was updated from &T / &x to @T / @x before supersession (see cluster report D1).

Summary

Add opt-in linear types to Metel. A value whose type is declared linear must be used exactly once — not silently dropped, not used twice. Linearity is checked statically as a second pass after type inference, with no runtime overhead. A narrow read-reference form @T (expression-only, non-storable) allows inspection without consumption. The default runtime-managed memory model is unchanged.

Motivation

Metel's default memory model is runtime-managed (reference counting). This is ergonomic for most code, but insufficient for systems-level use cases where:

• A resource must be explicitly released (file handles, sockets, buffers)
• Allocation and deallocation must be deterministic and zero-overhead
• Use-after-free and resource leaks should be caught at compile time, not at runtime

Linear types provide this without requiring the full ownership and borrow-checker machinery of Rust. The programmer opts in per type; all other code is unaffected.

Proposal

1. Declaring linear types

The linear keyword annotates a struct or enum declaration:

linear struct Buffer {
    ptr: Int,
    len: Int,
}

linear struct FileHandle {
    fd: Int,
}

linear enum Connection {
    Open { socket: Int },
    Closed,
}

Any value whose static type is linear is subject to the use-exactly-once rule. Non-linear types are unaffected.

A struct or enum that contains a linear field is itself treated as linear automatically. The linear keyword need not (and should not) be repeated on the outer type — it is inferred transitively:

struct Request {
    body: Buffer,    // Buffer is linear → Request is implicitly linear
    url: String,
}

2. Consumption

A linear value is consumed by any of:

• Passing it as an argument to a function
• Returning it from a function or block
• Binding it to a new name via let (the original binding becomes dead)
• Destructuring it in match or a let destructure

Consuming a linear value that has already been consumed is a compile error. A linear binding that reaches the end of its scope without being consumed is a compile error.

let f = FileHandle::open("data.txt");
f.close();   // consumed — ok

let f2 = FileHandle::open("data.txt");
// scope ends — ERROR: f2 not consumed

let f3 = FileHandle::open("data.txt");
f3.close();
f3.close();  // ERROR: f3 already consumed

3. Read references — @T

Without a way to inspect a linear value without consuming it, every method call would destroy the value. Full lifetime-tracked borrow checking is deliberately out of scope for this RFC. Instead, a minimal read reference @T is introduced with strict placement rules that make lifetimes unnecessary:

• @T is formed with the @ prefix operator: @expr
• @T may only appear in expression position — it cannot be bound to a let, stored in a struct field, or appear in a function return type
• @T is not itself linear — it may be used any number of times within its expression scope
• A function that accepts @T may read from the value but cannot consume it (it does not own it)

linear struct Buffer { ptr: Int, len: Int }

fun buf_len(b: @Buffer) -> Int { b.len }

let buf = Buffer::alloc(1024);
let len = buf_len(@buf);   // buf is not consumed; @buf is a temporary read view
buf.free();                // consumed here

Because @T cannot be stored, it cannot outlive the expression it appears in. No lifetime annotations are needed.

The @ sigil is distinct from & (address-of, RFC-0001): &x always produces a storable RC-backed *T; @x produces a non-storable read reference with no runtime representation. The two operators are unambiguous — & is for non-linear pointer semantics, @ is for linear read access.

Mutable references are out of scope for this RFC. Mutation of a linear value is done by consuming it and producing a new one (or by methods that take self and return Self).

4. Branching

Every branch of an if or match expression must leave all in-scope linear values in the same consumption state at the merge point. If a linear value is consumed in one branch, it must be consumed in all branches:

let buf = Buffer::alloc(1024);

if condition {
    buf.free();
    // ERROR: buf consumed here but not in the false branch
}

// Correct:
if condition {
    buf.write(data);
    buf.free();
} else {
    buf.free();
}

This rule applies to all arms of a match expression identically.

5. Loops

A linear value created outside a loop body may not be consumed inside it. The consumption count would be unpredictable (zero iterations, one, or many):

let buf = Buffer::alloc(1024);
for item in items {
    buf.write(item);  // ERROR: buf created outside; cannot consume in loop body
}

A linear value created inside a loop body is fine — it is created and consumed once per iteration:

for item in items {
    let conn = Connection::open(item.addr);
    conn.send(item.data);
    conn.close();   // ok — created and consumed within the same iteration
}

6. drop — explicit discard

To consume a linear value intentionally without performing any operation, use the built-in drop:

let buf = Buffer::alloc(1024);
drop(buf);   // consumed; satisfies the linearity checker

drop has the signature fun<T: Linear>(val: T). If T defines a destructor method by convention (e.g. free, close), drop does not call it — the programmer must call the destructor explicitly. drop is purely a linearity-checker escape hatch.

7. Destructuring linear types

Destructuring a linear value in let or match consumes the outer value and introduces each field as a new binding. Each extracted linear field must itself be consumed:

let Request { body, url } = req;   // req consumed; body is a new live linear binding
body.free();                        // body consumed
// url: String — non-linear, no constraint

Partially destructuring a linear struct (binding some fields and ignoring others with _) is only valid if the ignored fields are non-linear. Ignoring a linear field is a compile error:

let Buffer { ptr, .. } = buf;   // ERROR if len is linear or if Buffer has linear fields not bound

8. Runtime interaction

Linear values bypass the reference-counting runtime entirely. No Rc wrapper is allocated; no reference count is maintained. The backing resource is managed solely by the consuming function (e.g. free, close). The evaluator treats linear values as plain values — correctness is entirely a static guarantee.

9. Typechecker changes

A linearity environment (LinearEnv) is maintained alongside the existing type environment. It maps each in-scope binding to one of:

• Unconsumed — the value exists and has not yet been used
• Consumed(location) — the value was consumed at the given source location

The linearity pass runs after type inference (Pass 2), once all types are concrete and it is known which types are linear.

Rules:

Event	Action
let x = <linear expr>	Add x → Unconsumed to LinearEnv
Use of x where x is linear	If Unconsumed: mark Consumed(here). If Consumed: error — double use
@x (read reference)	Do not mark consumed; verify x is Unconsumed
Scope exit	For each linear binding in scope: error if still Unconsumed
if/match merge	Verify LinearEnv state is identical across all branches
Loop body entry	Snapshot linear bindings from outer scope; forbid consuming any of them inside the body

Alternatives Considered

Full ownership + borrow checking (Rust model)

Provides the strongest static guarantees but requires lifetime annotations, mutable references, and a borrow checker that understands aliasing. This is a significant language-level investment and changes the feel of the language for all users, not just those opting into manual memory management. Deferred indefinitely.

Owned<T> wrapper type

A library type Owned<T> wraps a value and requires explicit .free(). Simpler than linear types but enforced only by convention — the compiler does not verify that .free() is called, making leaks and double-frees possible. Linear types provide the same ergonomic opt-in with static verification.

Region/arena allocation

Allocate from a Region; all values in the region are freed together when the region is freed. Complementary to linear types rather than an alternative — a region could itself be a linear value. Regions avoid per-object tracking but cannot express single-object deterministic release. Tracked in RFC-0025 (docs/public/rfcs/rfc-0025-region-allocation.md).

unsafe blocks

Gate raw memory operations behind an unsafe boundary, as in Rust. Rejected as the primary mechanism — the goal is fine-grained control without requiring unsafe code, preserving a uniform safety story. However, unsafe blocks are a necessary complement for FFI, custom allocators, and cases the type system cannot reason about. Tracked in RFC-0026 (docs/public/rfcs/rfc-0026-unsafe-blocks.md). Inside an unsafe block, the linearity checker is relaxed — linear values may be aliased or dropped without consuming, with correctness asserted by the programmer.

Open Questions

1. Destructor protocol. Should the language define a Drop aspect with a drop(self) method that is called automatically when a linear value would otherwise go out of scope unconsumed — converting a compile error into an implicit call? This would ease migration but weakens the "must be explicit" guarantee.

2. @T mutability. This RFC introduces only read references. A mutable form @mut T is explicitly out of scope — mutation of a linear value is done by consuming and returning, which avoids the exclusive-lock tracking that @mut T would require. If this proves too restrictive in practice, a future RFC may revisit it.

3. Linear type parameters. Can a generic type parameter be constrained to linear: fun<T: Linear>(val: T)? This RFC assumes yes (it is needed for drop), but the interaction with v0.2 generics needs careful design.

4. Transitivity warnings. When a non-annotated struct becomes implicitly linear because of a linear field, should the compiler emit a warning or require an explicit linear annotation on the outer struct? Implicit propagation is convenient but may surprise users.

5. Error recovery. When a linear value is not consumed, should the compiler attempt to insert a drop call automatically and emit a warning rather than a hard error? This would make the system more lenient for early-stage code.

6. Mandatory vs. inferred drop. This RFC requires the programmer to call drop (or a consuming method) explicitly. An alternative is for the compiler to infer a drop call at the point where a linear value goes out of scope unconsumed — emitting a warning rather than an error, or silently inserting it when the type implements a destructor. The tradeoff: mandatory drop maximises explicitness and catches forgotten closes/frees at compile time; inferred drop reduces boilerplate for cases where the only goal is deterministic cleanup timing (e.g. a scoped lock). A middle ground is mandatory by default, with an #[auto_drop] attribute on the type declaration to opt into silent inference.

7. Linear vs. affine types. Linear (exactly once) and affine (at most once — may be dropped without consuming) are distinct disciplines. This RFC proposes linear semantics throughout. Affine types would allow a value to go out of scope silently — the compiler would not error on an unconsumed binding — while still preventing double-use. The benefit is a gentler model: affine types enforce no-aliasing and prevent use-after-free without requiring explicit cleanup. A possible design is two keywords (linear and affine) or a single keyword with a flag (linear(drop: optional)). The distinction matters most for types that carry no external resource (e.g. a unique token used for ordering guarantees) where silent drop is safe and desirable, versus types that own a file handle or socket where silent drop would leak.

Timing Recommendation

Linear types depend on generics (v0.2, RFC-0024 needs fun<T: Linear>). Target v0.4+ after generics and aspects are stable. The @T read reference form is syntactically resolved (see Conflict 1 in the cluster report — D1 decided). The @ sigil is distinct from & (RFC-0001 address-of).

References

• Language spec: docs/public/spec.md
• Type system spec: docs/public/spec/types.md
• Typechecker notes: metel-interpreter/docs/typechecker.md
• Related: RFC-0003 (concurrency model), RFC-0006 (closure capture semantics)
• RFC-0025: docs/public/rfcs/rfc-0025-region-allocation.md — Region is a linear type; bulk deallocation complement to per-object linear management
• RFC-0026: docs/public/rfcs/rfc-0026-unsafe-blocks.md — linearity checker relaxed inside unsafe; escape hatch for FFI and custom allocators
• Cluster report: docs/internal/rfc-cluster-memory-model.md
• Prior art: Linear Haskell (Bernardy et al. 2018), Rust ownership model, Cyclone regions