Linearity and Control
— 2023-03-23

1. introduction
2. what are linear types?
3. create and consume
   1. linear types
   2. linear functions
   3. linear contexts
   4. linear methods
   5. linear drop
4. control
   1. control points
   2. liveness
   3. abort points
5. async and linearity
6. cycles and safety
7. closure captures
8. linear stdlib
9. movability
10. further reading
11. conclusion

Introduction

Update 2023-03-28: I've published a follow-up to this post which presents an alternate design, reframing linearity as: "Drop is guaranteed to run". To get a full overview of the design space, read this post to get a sense of the problem domain, and the follow-up post for a concrete solution.

---

A week ago Niko published a post on linear types, introducing the idea of "must move" types, which he suggested could be implemented through some form of ?Drop bound. It's far from the first time linear types have come up. Five years ago Gankra also published a post on linear types, explaining what they are and why they're hard to get right.

In this post I want to build on these two posts; expanding on what linear types are, why they're useful, how they would interact with Rust, and share a novel effect-based design — which unlike many previous attempts would preserve our ability to implement and use destructors.

Before we dive in I want to extend an enormous thanks to Eric Holk, for first positing the idea that linearity obligations might be transferable up the call stack or ownership chain. That has been the key insight on which the majority of the design in this post builds.

⚠️ Disclaimer: The syntax in this post is entirely made up, and meant as illustrative only. While it may be tempting to discuss syntax, this post is primarily focused on semantics instead. I am not a member of the language team. I do not speak for the language team. This post does not encode any decisions made by the language team. The point of this post is to exchange ideas, in the open, with peers - because in my opinion that is the best way to go about designing things.️

What are linear types?

If you've been writing Rust for a little while, you'll be familiar with #[must_use]. Decorating a function with this attribute makes it so the types returned from the functions must be used or else it produces a warning. But #[must_use] is limited. "using" in this context means "doing literally anything with the function output". As long as we do that, #[must_use] is happy. This includes, or example, passing it to mem::forget or Box::leak.

must_use_fn();              // ⚠️ "unused return value of `must_use_fn` that must be used"
let x = must_use_fn();      // ✅ no warnings or errors
let _ = must_use_fn();      // ✅ no warnings or errors
mem::forget(must_use_fn()); // ✅ no warnings or errors

However there are often cases where we would like a more rigorous version of #[must_use]. Say we have a Transaction type. It has a method new to create a transaction, a method commit to finalize the transaction successfully, and a method abort to finalize the transaction unsuccessfully.

/// A type representing a transaction.
struct Transaction { .. }
impl Transaction {
    /// Create a new instance of `Transaction`.
    fn new() -> Self { .. }
    /// Finalize `Transaction` successfully.
    fn commit(self) { .. }
    /// Finalize `Transaction` unsuccessfully.
    fn abort(self) { .. }
}

What we'd like to express here is that if you call new, you must call either commit, or abort. But Rust's type system doesn't let us express this yet. Even Drop wouldn't help us here, since the type system doesn't guarantee it'll ever be called. What we'd like is for the following to be possible:

let _ = Transaction::new(); // ❌ "unused return value of `Transaction::new` that must be used"

The reason for this is that Rust type system supports affine types, but does not support linear types. This is a common misconception, but the difference between them is actually pretty important:

• affine types are types which must can be used at most once.
• linear types are types which must be used exactly once.

This means that Rust can guarantee you won't use the same type twice (e.g. we systemically prevent double frees from happening); but for example we can't guarantee that values will have methods called on them (e.g. we can't prevent memory from leaking). Being able to express linearity in Rust would likely also enable us to solve some of the other challenges we've been facing:

• async scopes: thread::scope allows us to share variables between threads without using locks. An async/.await version of this would require linear types to function ¹.
• true session types: This is best explained as: "What if we could model the semantics of entire network protocols using the type system." We can get close today, but to fully encode session types we require access to linear types [^session-type-limits] ².
• more efficient completion-based IO: APIs such as io_uring have very specific rules about how objects should be passed between the kernel and the program. Linear types should make it possible to model these interactions with significantly less runtime overhead ³.
• more efficient async C++ FFI: The Future-equivalent in C++ must be polled to completion because if you don't you trigger UB. This is unlike Rust's Future type which can be dropped to be cancelled. Linear types would allow us to model this behavior directly in Rust's type system.

To provide a quick example of something which is inexpressible in Rust today: we can't create an async/.await version of thread::scope in Rust today. But using linear types, we could require that the future returned by async_scope is awaited, and that in the event of a cancellation, the destructors of async_scope are guaranteed to run for as long as tasks are live, ensuring we maintain Rust's property of preventing all data races in safe Rust ⁵.

let mut a = vec![1, 2, 3];
let mut x = 0;

async_scope(|s| {
    s.spawn(|| {
        println!("hello from the first scoped task");
        // We can borrow `a` here.
        dbg!(&a);
    });
    s.spawn(|| {
        println!("hello from the second scoped task");
        // We can even mutably borrow `x` here,
        // because no other tasks are using it.
        x += a[0] + a[2];
    });
    println!("hello from the main task");
}).await;

// After the scope, we can modify and access our variables again:
a.push(4);
assert_eq!(x, a.len());

Create and consume

Okay, time to get into the details of the design. At the heart of a linear type's lifecycle are two phases: create (or "construct") and consume (or "destruct"). A linear type promises at the type system level that once it's created, it will always be consumed. The way we're modeling this in our design is using type instantiation to create and pattern destructuring to consume

let txn = Transaction { .. };  // 1. Create a new instance of `Transaction`.
let Transaction { .. } = txn;  // 2. Consume an instance of `Transaction`.

No matter what happens in the code, every linear type which is created will always have a matching consume. This means that as long as your program has an opportunity to run to completion it is guaranteed to be consumed. Yay for type systems!

In this post we'll be modeling this via the introduction of a new effect kind (or "modifier keyword" if you prefer): linear. Don't worry too much about the name, I'm mostly using it for clarity throughout this post. This effect can be applied to either types or functions; but we'll start with types.

Linear types

When a type is marked as linear it means that once a type has been created, in order for it to type-check it must also be consumed. This will be automatically done by the type checker for you, who will gently tell you if you messed up anywhere. But by using unsafe you can also do this by hand if you need to. More on that later though.

linear struct Transaction { .. }
linear enum Foo { .. }

This is not the end of linear types though: a key feature of types is that they can be composed into new types. When a type takes a linear type as an argument, the "linearity" obligation transfers to the enclosing type. This means that a linear type can only be held by another linear type:

linear struct TransactionWrapper {
    txn: Transaction, // linear type
}

Linear functions

The second place where the linear notation can be used is on functions and methods. The way this would look is like this:

impl Transaction {
    fn new() -> Self { .. }
    linear fn commit(linear self) { .. }
    linear fn abort(linear self) { .. }
}

Functions which don't take any linear types as arguments don't have to be marked as linear fn which is why fn new is not marked linear here ⁷. But if a function wants to take a linear type as an argument, it needs to be marked as a linear fn. Every linear function needs to promise it will do one of three things for every instance of a linear type which is passed to it:

1. It will destruct the instance.
2. It will yield the instance to the caller along with control over execution.
3. It will call another linear function and pass the instance along as an argument.

This might sound easy enough, but in practice this has implications for what can't be done, such as:

1. It will not mem::forget any instances of linear types.
2. It will not create any cycles around instances of linear types using Arc/Rc or similar.

If we can imagine a parallel version of the stdlib where all types and functions which can be linear are in fact linear: mem::forget, Arc::new, and Rc::new would not exist. And our safety rules would disallow creating new linear fns which don't uphold those rules. Being able to mark which functions uphold the rules of linearity is exactly the purpose of the linear fn notation.

Linear contexts

The "must consume" obligation of a linear function only applies to arguments which themselves are also linear. It should be possible to pass non-linear arguments to linear functions without any problem, allowing you to mix and match linear and non-linear types within a linear function.

Similarly: it should be possible to create linear types and call linear functions from non-linear functions. This means you should be able to create and consume linear types from your existing functions largely without problems. The exceptions here are probably async contexts, and things like closure captures: both of those create types which wrap existing types. So when they capture a linear type, they themselves must become linear too. We'll get into more detail on how that works later on in this post.

This means that it should be possible to for example have an fn main which is not marked linear which creates and consumes linear types in its function body:

fn main() {                        // 1. Non-linear function context.
    let txn = Transaction { .. };  // 2. Create a new instance of `Transaction`.
    let Transaction { .. } = txn;  // 3. Consume an instance of `Transaction`.
}

If for whatever reason we do find a good reason why linear types should only be accessible from linear contexts, we could do that. Just like with const {} we could create a linear {} context which can be used to close out the linearity effect. But I don't think that is necessary, and I suspect linear types would be easier to use if we didn't require this. This is almost a question of syntax though, so it's probably not worth going too deep into this right now.

Linear methods

I've sort of hinted at this, but not said it out loud: for linear types to be really useful it's not enough if we have types which cannot be dropped. What we really want is pairs of methods which need to be called.

In Rust we don't have "class constructors" built into the language as a feature. Instead what we have is struct initialization, and methods such as MyStruct::new or MyStruct::open to construct the type. The reason why these work is because they're the only places in the code which have access to the struct's private fields. So to create the struct, they're the only way to do it.

impl Transaction {
    pub fn new() -> Self { 
        Self { field1, field2 }
    }
}

Similarly with linear types what we don't want is for people to require access to private fields to destruct their types. Instead we can just create methods which can do the destruction for us. This means that the only way to close out the linear effect's requirements is to call a destructor method on the type:

impl Transaction {
    pub linear fn commit(self) {
        let Self { field1, field2 } = self;
    }
    pub linear fn abort(self) { 
        let Self { field1, field2 } = self;
    }
}

As we discussed earlier: the only valid thing to do with an instance of a linear type is to either consume it, return it, or pass it to another linear function. "linear destructors" do the latter: they're linear functions which consume a linear type. So from a compiler's perspective this is exactly right.

Linear drop

A key feature feature in Rust is the ability to define Drop destructors (RAII). For example when you create a file using File::open, its Drop destructor will make sure that the file is closed when it goes out of scope. Syntactically this makes code a lot nicer to read, because rather than needing to remember which function to call inside a function body, the type implementing Drop will just auto-cleanup all resources for you.

To ensure "linear Rust" is as ergonomic as non-linear Rust, code should largely feel the same as well. This includes having access to Drop. The way we could do this is by introducing a linear version of Drop, which rather than take &mut self takes self. And when called requires the existing rules of linearity are upheld. The way this destructor would work is that it would only run when a type goes out of scope. It would not run if a type is manually destructed.

People may be wondering at this point what the difference between linear types and affine types then is, if both get access to destructors. With affine types we can't guarantee that destructors will run, so we can't build on it for the purpose of soundness. With linear types we can make that guarantee, so we destructors can be relied on for the purpose of soundness.

In our Transaction example, we can imagine that we might to abort the transaction unsuccessfully if it goes out of scope. But we would want to successfully commit it by hand if we've succeeded. We could do that by adding the following linear Drop implementation:

impl linear Drop for Transaction {
    fn drop(linear self) {
        self.abort(self);
    }
}

This would make it so if the transaction goes out of scope or if we call abort it aborts. But only if we call commit manually does it complete successfully:

fn do_thing() -> Result<()> {      // 1. No linear arguments, so no `linear fn` needed.
    let txn = Transaction::new();  // 2. Create a new transaction.
    some_action()?;                // 3. On error, drop `txn` and call the destructor.
    txn.commit();                  // 4. On success, call `txn.commit`.
    Ok(())                         // 5. Return from the function; no linear types are live.
}

Admittedly I'm not entirely sure whether linear Drop in fact requires taking linear Self to be destructed, or whether it would suffice for Drop to keep taking &mut self as an argument, assuming that if the destructor is called, it will be destructed anyway. The most important difference between linear Drop and regular Drop is that linear Drop will not run if the type is manually destructed. And that unlike regular Drop, linear types guarantee they will be destructed. The exact details of the interfaces are secondary to the semantics we're trying to encode.

Control

In this section I'll be covering the interactions of linear types with control-flow primitives such as panic and async. Creating a coherent model for their interactions is a requirement to make linear types practical.

Control Points

You may have heard of the term "control flow" to refer to things like branches, loops, and function calls. It describes the "flow" of control over execution. Perhaps you've also heard of "control flow operators" to refer to things like if, while, and for..in which are the specific keywords we use to encode control flow operations. In the compiler all of these things are tracked in a data structure called the "control-flow graph" (CFG).

I've found there is a term here missing, which is something I've started calling "control points": places in the code where the callee hands control over execution back to its caller. The caller then may or may not hand control back to the callee ⁸. Not all control-flow operations are equal though. We can divide them into two categories:

• Breaking operations: hand control back to the caller, and that's it. Examples: return, break, continue, ?, panic!.
• Suspending operations: hand control back to the caller, but the caller can choose to hand control back to the callee again later. Examples: .await, yield.

I'm using "caller" and "callee" somewhat loosely here, since Rust is expression-oriented and with things like try {} blocks and inline loop {}, control flow doesn't necessarily need to be handed to a different function. It can be enough to be handed to an enclosing scope. Let's take a look at a reasonably representative Rust function which does some async IO and then some parsing:

async fn do_something(path: PathBuf) -> io::Result<Table> {
    let file = fs::open(&path).await?;
    let table = parse_table(file)?;
    Ok(table)
}

And here it is again, with all control points fully annotated:

async fn do_something(path: PathBuf) -> io::Result<Table> {
                                        // 1. futures start suspended, and may not resume again
    let file = fs::open(&path).await?;  // 2. `.await` suspends, and may not resume again
                                        // 3. `?` propagates errors to the caller
                                        // 4. `fs::open` may panic and unwind
    let table = parse_table(file)?;     // 5. `?` propagates errors to the caller
                                        // 6. `parse_table` may panic and unwind
    Ok(table)                           // 7. return a value to the caller
}

While many of the control points in this function are visible, many others are not. In order for linear types to function, they need to account for all control points regardless of whether they're visible or not. This is why it's so important to be able to implement linear Drop destructors. Because without them it wouldn't be possible to carry linear types over control points.

Liveness

Now that we've covered what control points are, we can discuss how they interact with linear types. In its most basic form: when a linear type is held live across a control point, the compiler cannot prove that it will be consumed. Assuming we take our earliest version of Transaction which didn't implement linear Drop. If you hold a an instance of it across an .await the compiler should throw an error. The ? may cause the function to return, meaning there is no guarantee txn.commit will ever be invoked:

fn do_something() {
    let txn = Transaction::new();  // 1. Create an instance of `Transaction` (assuming no `linear Drop`).
    some_action()?;                // 2. ❌ `?` may cause the function to return with an error.
    txn.commit();                  // 3. ❌ we cannot guarantee `txn.commit` will be called.
}

This is the reason why in order for linear types to be practical, they must implement a form of "consuming Drop". Without it we couldn't hold any linear types across control points. And because every function in Rust is currently allowed to panic, it means having linear types without destructors would be entirely impractical. That's why its likely virtually every linear type will want to implement some form of linear Drop, and there are open questions on how deeply we could integrate this into the language:

fn do_something() {
    let txn = Transaction::new();  // 1. Create an instance of `Transaction` (assuming `linear Drop`).
    some_action()?;                // 2. ✅ `?` may cause the function to return with an error, invoking `txn.drop`.
    txn.commit();                  // 3. ✅ Or `?` does not return, and `txn.commit` is called.
}

The key interaction between linear types and control points is one of liveness. When interacting with a control point, linear types must guarantee they will remain live. This means the linear type must either being returned from a scope via the control point, or must be able to be destructed before the control point finishes handing control back over (e.g. linear Drop). I hope the terminology of "liveness" and "control points" can provide us with the missing vocabulary to talk about how linear types interact with things such as panics and errors.

Abort points

It's important to distinguish between "control points" and what I'm calling here: "abort points". Where control points represent points in the control-flow graph where control over execution is handed off to another place within the program. "Abort points" represent points within the program at which point the program stops executing entirely.

In practice, every line of code represents an abort point. There is no guarantee a computer will execute the next instruction on a CPU. The best it can do is guarantee that if a next instruction will be run, which one it will be. Power plugs can be pulled, CPUs can shut down processes, kernels can crash. These are things which live outside the type system, and we cannot model within the type system. The type system assumes that the hardware it runs on is well-behaved. If it isn't, the model doesn't hold.

When we write panic=abort in our Cargo.toml it changes the meaning of panic! from "unwind" to "just immediately stop". Similarly: we can use std::process::exit to stop a program then and there. Because we exit the confines of the program, the type system cannot meaningfully say anything about it, so linear types can't model it.

Similarly: we can't treat slow operations as control points either. If a program runs thread::sleep(10_years), as far as the type system is concerned that doesn't represent a control point anymore than thread::sleep(10_nanos) would. The only time we can really capture that a linear type is violated is in the case of unreachable code. Take for example the following example:

fn do_something() {
    let txn = Transaction::new();  // 1. Create an instance of `Transaction`.
    loop {}                        // 2. Loop infinitely
    txn.commit();                  // 3. Complete the transaction.
}

… which should probably produce an error like this:

error: linear type destructor is unreachable
 --> src/lib.rs:4:1
  |
3 | loop {}
  | ------- any code following this expression is unreachable
4 | txn.commit();
  | ^^^^^^^^^^^^^ unreachable destructor
  |

Async and Linearity

Async Rust provides us with the ability to write non-blocking code in a imperative fashion, and through its design unlocks two key capabilities:

1. The ability to execute any number of async operations concurrently.
2. The ability to cancel any operation before it completes by dropping its corresponding future.

"async", much like "linearity" can best be thought of as an effect. And when we talk about combining async an linearity, what we're really discussing is effect composition. Effects are built into the language, and hold a deep semantic relationship to the underlying program. This means that when they interact we get to choose how they should behave together. In the case of composing linear and async, there are two behaviors we want to be able to encode:

1. must-await futures: these are futures which must be awaited, but once awaited may still be cancelled. Because cancellation is a very useful property for most kinds of futures.
2. must-consume futures: these are futures which not only must be awaited, even if attempted to be cancelled, they must continue doing their work.

In order for a future to be .awaited, it must first be "stack-pinned", resulting in a Pin<&mut T> type. In the general case this means we've permanently lost access to the inner T type: once a type has been pinned, it must remain pinned until it's dropped. This means that once we start polling a future, we can no longer destruct it. That's why for async Rust we need to expand the destructor rules of linearity slightly. In order to "consume" a linear future, it should be enough to place it inside a .await expression. Awaiting a future should be considered equivalent to consuming a future, even if we cancel it later on. This provides us with "must-use" futures:

let _ = meow();  // ❌ "`meow` returns a `Future` which must be `.await`ed"

In order to encode "must-consume" futures we will need access to an async version of linear drop. As Sabrina Jewson pointed out before: if we require a future to continue doing work when cancelled, it can continue doing that work in its drop handler. If the drop handler itself is un-cancellable, then we are able to construct un-cancellable futures.

Unlike the linear Drop we've shown before, async linear Drop cannot take self by-value because of the pinning rules. It instead it can only really take &mut self. So again, the fact that it's being destructed will need to be guaranteed by the fact that it's .awaited. Encoding the linearity of async linear Drop itself is a different matter. And I suspect we'll need to dedicate a separate post to exactly spell out how that should work. My guess is that this will require a connection that is as deep to the language as non-async Drop. And that at the root of the program it will bottom out in something like it being a linearity violation if you don't handle the future returned by Drop to completion. I'm not exactly sure yet how this should be done, but it seems like it should be doable.

Cycles and Safety

Unsafe Rust provides access to raw pointers. These are pointers, which unlike references, may alias if you're not careful. But just because they could alias doesn't mean they're allowed to alias. And it's in fact undefined behavior if you fail to uphold Rust's safety rules in unsafe Rust. unsafe only removes the guard rails, it doesn't change the rules.

The same would apply to linear fn/linear T and unsafe. It should be possible to cast a linear T to a regular T, if you make sure to keep treating T as if it was a linear T. This would allow you to create linear functions which internally could hold cycles, but which externally would not be observable. Assuming we had a "make this type non-linear" (UnsafeNonLinear) equivalent to UnsafeCell. We could imagine we could take an instance of Transaction and place it inside an Arc somewhat like this:

let txn = Transaction::new();                     // create a new linear transaction
let txn = unsafe { UnsafeNonLinear::new(txn) };   // cast it to remove its linearity
let txn = Arc::new(txn);                          // place it inside an `Arc`, *may* lead to cycles
let txn = Arc::into_inner().unwrap();             // extract it from the `Arc`
let txn = unsafe { txn.into_inner() };            // convert it back to a linear type

I don't really know whether it makes most sense to create an unsafe wrapper type, or whether we could use as-casts to peel the linearity effect. I would expect casting a T -> linear T would probably be safe, but I don't know for sure. Because this would be a new language construct we would be able to define all of these rules. They seem like they should be fairly straightforward, so fingers crossed it actually ends up being that way.

Finally there's an open question we have is whether it could in fact be possible to create linear versions of Arc and Rc (and Mutex/RefCell). If every cloned instance had to prove it was consumed, would it be possible to guarantee that no cycles may occur? Even if that's not possible for the existing APIs, perhaps a different formulation could provide those guarantees. Something like a scope API might be able to provide such guarantees. If this were possible it would make linear APIs significantly more convenient to use, so I suspect it would be worth examining this further.

Closure captures

An interesting challenge Gankra shared on Twitter is how closure captures interact with linearity. In order for "linear Rust" to be as ergonomic as non-linear Rust, the two should feel largely similar when used. This means closures and closure captures should be accessible from linear Rust too.

Let's examine an example more closely. Here is the Option::map function as implemented in the standard library today. It takes an Option, and a closure, and if Some applies the closure to it. If we take the None branch, at first glance it seems like nothing will happen. But on closer inspection we may realize that we drop the closure, and so we also drop all variables captured by the closure:

impl<T> Option<T> {
    pub fn map<U>(self, op: impl FnOnce(T) -> U) -> Option<U> {
        match self {
            Some(t) => Some(op(t)),
            None => None,
        }
    }
}

In Niko's blog post, this example was adapted to use T: ?Drop. This is valid because in the Some case the T parameter is passed to the closure, which can consume the linear type. While in the None case there is no T, so there is no type to consume. But as we've mentioned this does not account for the variables captured by the closure, which in this formulation would likely just be disallowed from performing any captures. Instead, using the linear effect we can model this the way we would expect because we have access to linear destructors, and because a linear type can only be captured by another linear type:

impl<linear T> Option<T> {
    pub linear fn map<U>(self, op: impl linear FnOnce(T) -> U) -> Option<U> {
        match self {
            Some(t) => Some(op(t)),
            None => None,
        }
    }
}

Because T is linear, the closure FnOnce which takes T as an argument must also be linear, and in turn the map method must be linear as well. This does assume that linear closures can be dropped to run the destructors of the variables they've captured. Which seems reasonable, since the Fn-family of traits are marked #[fundamental] and are part of the language - so we can define how they should function in the presence of linear.

Linear stdlib

Our linear fn map example doesn't quite capture the same semantics as Niko's proposal yet. This syntax requires types to be linear, whereas in Niko's version types may be linear - or they may not be. In order to capture this "maybe-ness" of effect keywords we need a way to express it: which is what the Keyword Generics Initiative has been working on.

To make our effect-based design of Option::map fully compatible with the semantics Niko laid out, we'd have to make one more change. Rather than using T: ?Drop which communicates the presence of an effect through the absence of an auto-trait, we can instead use ?linear T to more directly communicate the potential presence of an effect:

impl<?linear T> Option<T> {
    pub ?linear fn map<U>(self, op: impl ?linear FnOnce(T) -> U) -> Option<U> {
        match self {
            Some(t) => Some(op(t)),
            None => None,
        }
    }
}

From the feedback we've received I know many people are not particularly thrilled about this syntax - which is perfectly understandable. But exact syntax aside, it's important to observe that if we do this right, then this syntax should be mostly temporary. Aside from a few exceptions in the stdlib (Arc, Rc, mem::forget), most library code can probably be marked as linear. Which begs the question: if most code can be linear, could it make sense to eventually assume linearity, unless people opt-out? If that were the case, then the signature of Option::map would remain identical to what it is today in the stdlib already. But the signature of mem::forget could then become:

pub const fn forget<T: !linear>(t: T) { .. }

It seems far more desireable to gradually linear-ify the stdlib rather than defining a parallel linear stdlib checked into crates.io (as we've done once already for async). And far more empathic than trying to argue that users of Rust are in fact wrong for wanting to make use of APIs such as Option::map in linear contexts. Regardless of which set of effects you're using in Rust to program with, familiar patterns and techniques should be accessible to all.

Movability

In his post Niko describes "linear types" as "must-move types". This begs the question: if there are types which must move, are other kinds of moves possible as well? And there are. By default types in Rust can be described as "may-move types", because they can be moved but they don't have to. And then we also have access to "must-not-move types" which are represented by combining the Pin type with the !Unpin trait. Though in practice most people prefer to encode the immovability of types using the more declarative pin-project crate instead.

• must move: linear types
• may move: the default mode of Rust types
• must not move: pinned types

Thinking of "must-move types" (linear) as the opposite of "must-not-move types" (pinned) is a useful model to carry forward, as they encode opposing guarantees about the movability of types. Reconciling these opposing guarantees is what makes combining async + linear types difficult, since once futures start being polled can generally no longer be moved. If this post continues into a series, this would be a topic I'd like to revisit in more detail later on.

Further Reading

Gankra wrote an excellent post in 2015 on why mem::forget should be safe, explaining why we can't assume destructors will always run in Rust. She wrote a follow-up post in 2017 about what makes linear types hard to model, concluding on an optimistic note with: "Ok having actually written this all out, it’s better than I thought."

The Wikipedia page on linear types provides a useful overview of the difference between among other "linear" and "affine" types. Including type systems with both more and less guarantees than both. Phil Wadler's "linear types can change the world!", provides a great type-theoretical introduction to what linear types are, and why they are useful. Similarly on type-theory side, Phil Wadler also published "Propositions as Types" (paper, talk), making an excellent case that properties such as lambda calculus and linear types are not invented - they are discovered. Meaning they may in fact be a fundamental part of logic and computing.

More recently Tyler Mandry wrote a blog post on the challenges of defining scoped tasks in Rust. And Niko Matsakis wrote a post on "must move" types, as a potential way to overcome the challenges scoped tasks present. Miguel Young de la Sota gave a talk about move constructors in Rust, explaining how like in C++, Rust could implement self-referential types which can be moved. Yosh Wuyts (hello) wrote a post on the challenges we face in order to make common interactions with pinned values safe. Sabrina Jewson wrote a post describing the challenges of async destructors, going into great detail about various considerations in the design space. And Yosh Wuyts (hello, again) wrote a post describing how async cancellation works, and why it's an essential capability of async Rust.

Conclusion

Linearity in Rust is largely inexpressible today. This leads us to work around this restriction in various ways, which come at the cost of correctness, performance, and ergonomics. In this post we've shown how linearity in Rust could be modeled as an effect, bypassing any of these restrictions. We've shown how it could be used to create ergonomics which are largely similar to existing Rust, and how we could gradually introduce linearity into the stdlib and ecosystem.

We've shown how for the sake of ergonomics it's not only important to be able to create and consume bare types, but also to be able to define constructors and destructors which must be called as pairs. Another contribution this post has made is formulated a model for linear Drop; which is required to preserve Rust's existing ergonomics in a linear context.

Finally we've taken a closer look at how linearity interacts with cycles, with unsafe, and with async. For async specifically, we've taken a look at how linear async fn would work, why it should not disallow cancellation by default, and how we could use it to still encode "must-not cancel" semantics.

To close this post out: I don't expect this post to function as a definitive design. In fact, it was written with the opposite intent. I hope this post will help us better understand the challenges linear types face in Rust, and serve as a useful tool in getting us closer to a design which we would be happy to adopt.

I'd like to thank Sy Brand, Iryna Shestak, and Eric Holk for reviewing this post prior to publishing.