Linear Types One-Pager
— 2023-03-28

  1. prior reading
  2. what are linear types?
  3. a minimal implementation
  4. interactions with control flow
  5. drawbacks and challenges
  6. updates

This post represents an overview of an MVP "linear types" design which we could probably start implementing and validating today if we wanted to. What I'm sharing here is a combination of conversations I've had with Gankra and Jonas Sheevink.

Prior Reading

What are linear types?

We typically frame linear types as: "Real #[must_use] types". But it seems like what we should be doing is framing linear types as: "Types which guarantee their destructor will be called." This is enough to provide the benefit we feature we actually want: a guarantee that destructors will be called, so we can rely on them for soundness purposes.

A minimal implementation

The estimate is that something like this would probably take a skilled compiler engineer on the order of days, not weeks or months, to validate:

This wouldn't require any special type of Drop either, we just guarantee it will always be called for all !Leak types. I have a feeling this design is actually really close to what Niko was describing in his post. The main difference is that we consider a destructor being run as enough to satisfy the "must use" semantics of linear types. So the only difference between linear and affine types is that linear types can't be safely passed to APIs such as mem::forget and Arc::new.

Interactions with control flow

The only way to prevent Drop from running is if we pass it to mem::forget, create a cycle using Rc, Arc, or using static. The first relies on the ManuallyDrop built-in, the second relies on the UnsafeCell built-in, and the last is a language item. We can disallow the use of !Leak types in static lang items. And for the functions we can make it so the bounds will always need to take + Leak, meaning all of their derivatives will too. If a function wants to use take ?Leak as a bound and pass it to + Leak types, the only way to do that is via an unsafe cast. That would mean it is on the hook for upholding the safety invariants of the ?Leak type. All other interactions with e.g. panic!, .await, or ? would Just Work as expected and we don't need to do anything for them.

If people want to put a !Leak type in an Arc, they can create an unsafe wrapper which temporarily removes the !Leak bound from the type, and put that in an Arc. They'd then be manually on the hook for ensuring destructors are run, but that's okay.

For async types, we don't yet have a async Drop design. But !Leak types would guarantee that async Drop is always run. This would be enough to guarantee the "must consume" semantics we want for certain types.

Drawbacks and Challenges

This scheme would work and could be implemented in record time. In my opinion we should do this on nightly, just to prove that it can be done. Once done we can tackle the ergonomics issues this creates:

I believe that just like with dyn, "must not move", send, etc we should look at an alternate formulation of these bounds by treating them as built-in effects. That would allow us to address the issues of versioning, visual noise, etc. in a more consistent and ergonomic way. But that's not a requirement to start testing this out, so if we believe we want this feature, starting with the design in this document seems to me like the right way to go.

Updates

update 2023-05-03: Jack Rickard pointed out that !Leak types and statics have bad interactions. Types which are placed in statics don't have their destructors run when the program exits. Which means that if we allowed !Leak types to be placed inside statics, it would prevent destructors from running entirely. This would break the linearity guarantees. so statics have to be a no-no for linear types. This puts linearity right next to const in that statics are fundamentally disallowed.

2023-05-04: From talking more to Jack Rickard, we created another example of "safe forget" using thread::spawn:

fn safe_forget<T>(val: T) {
    thread::spawn(move || {
        let val = val;                   // move `val` into the thread
        loop { std::thread::park(); }    // park the thread indefinitely
    });                                  // drop the thread thandle
}

The thread handle becomes unreachable, detaching the thread, and holding the value until the main thread exits - at which point destructors won't run 1. This is contrast to thread::scope, which is tree-structured and wouldn't allow doing this. To me this seems to indicate three things:

  1. In order to guarantee destructors are run, it's key to prevent cycles. This holds for both data (Rc/Arc) and computation (thread::spawn). I've got a hunch that structured concurrency is very closely connected to what we're trying to do here.
  2. If we are to introduce linearity into Rust, we need to follow the path we've taken with const. One API at the time, validating the linearity guarantees at each stage. This emphasizes the need to have a formalization of the safety rules.
  3. Even in this model we need to have a way to express ?Leak Fn to enable closing over !Leak types. This adds further credibility to the idea that we will want some form of surface syntax for !leak fn, to be able to declare free functions which can be passed into linear closure position. This is in addition to the existing !leak async fn use case.
1

It makes me wonder about an alternate timeline where JoinHandle would be !Leak and implement "join on drop" semantics. Had that been the case, then thread::spawn would probably have been okay to close over !Leak types.