Linear Types One-Pager
— 2023-03-28
- prior reading
- what are linear types?
- a minimal implementation
- interactions with control flow
- drawbacks and challenges
- 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:
- We define a new
unsafe
(auto-)trait namedLeak
/Leave
/Forget
- All bounds take an implicit
+ Leak
bound, like we do for+ Sized
. - Certain functions such as
mem::forget
will always keep taking+ Leak
bounds. - Functions which want to opt-in to linearity can take
+ ?Leak
bounds. - Types which want to opt-in to linearity can implement
!Leak
or put aPhantomLeak
type in a field.
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:
- We would want to go through the entire stdlib and mark almost every
generic param as
+ ?Leak
. - Because trait bounds are instantly stable, we would have no trial period to test out a linear bound, before committing to it.
- Just like how
?Sized
describes "maybe-dyn",?Leak
describes "maybe-must-move". Because we're talking in terms of negation, it is really hard to reason about. Our dyn system is notorious for being some of the hardest to understand part of Rust. - Assuming all but a few bounds in the stdlib will eventually take
?Leak
, will we ever want to switch to make that the default across an edition to reduce line noise? If we think we might, we should think about what that would look like. Leak
introduces new safety rules for Rust which must be upheld when declaring?Leak
or!Leak
bounds. Those will need to be spelled out in detail beforeLeak
can be stabilized.
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:
- 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. - 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. - 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.
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.