Thanks to all the commenters on the previous proposal. All the feedback certainly helped me to consider cases that hadn’t previously occurred to me, and to (hopefully) improve the ergonomics considerably. Here is my second try:
- Start Date: 2015-01-14
- RFC PR: (leave this empty)
- Rust Issue: (leave this empty)
Summary
Add a linear attribute for compound type items. Linear types must be explicitly consumed or moved in every stack frame in which they are encountered. (They are not allowed to be in a “possibly moved” state.) Construction of variables with linear types is identical to construction of ordinary compound variables, while consuming a linear type can be achieved by moving its contents out of the linear compound structure. Extend support for kind-sigils.
Motivation
Scope-based drop is an implicit mechanism for ensuring that Rust programs do not leak resources. For the most part, this implicit mechanism works very well. However, when drop has side-effects that are important for program correctness (for example, a MutexGuard that releases a shared mutex when it is dropped), implicit drops will not communicate developer intent as effectively as explicit action. linear types provide a means for library authors to communicate to library clients that resource clean-up will have side-effects that are important for program correctness, and will document in client code the explicit design considerations that have been made regarding resource clean-up.
I have seen some resistance to the idea that scope-based clean-up may be inadequate, so I’ll try to address that here.
When is scope-based drop inappropriate?
Scope-based drop is inappropriate in scenarios where resource clean-up has side-effects whose timing can affect program correctness. For example, a MutexGuard will release a shared mutex when it is dropped. The scope of time in which a shared mutex is locked is a highly important consideration in writing correct multi-threaded code, and highly important considerations such as this should be explicitly reflected in code.
Example: Force explicit mutex drop.
To take an example from RFC #210:
let (guard, state) = self.lock(); // (`guard` is mutex `LockGuard`)
...
if state.disconnected {
...
} else {
...
match f() {
Variant1(payload) => g(payload, guard),
Variant2 => {}
}
... // (***)
Ok(())
}
(source)
In this code, it is impossible to discern whether the author intended or did not intend for the MutexGuard to be held in the ... // (***) code region. Developer intent could be properly signalled in two ways:
- If the developer intended that the lock possibly be held for the
(***)code, he could wrap the guard in anOption. This solution is well understood, I don’t feel I need to spend more time on it here. - If the developer intended that the lock not be held, he should enforce that each branch of the
matchabove cause a drop.
There is currently no way for rust to help the programmer to enforce case 2. With linear types, this could be handled as follows:
let (guard, state) = self.lock(); // (`guard` is mutex `LockGuard`)
...
if state.disconnected {
...
} else {
...
let linear_guard = Linear(guard); // (`guard` moved into linear_guard)
match f() {
Variant1(payload) => g(payload, linear_guard),
Variant2 => {
// Unless the `drop` is uncommented, compilation will
// fail with:
// ERROR: linear type `linear_guard` not fully consumed by block.
//drop(linear_guard.deref_move())
}
}
... // (***)
Ok(())
}
// existing drop rules enforce that `guard` would be dropped
// as it leaves scope.
This signals developer intention much more clearly, and allows the compiler to help the developer prevent a bug in the old code.
Example: Force explicit variable lifetime for FFI.
Consider this example:
extern {
fn set_callback(cb:|c_int|, state:*const c_void);
fn check(a:c_int, b:c_int);
}
fn main() {
let r = |x:c_int, data:*const c_void| {
let foo:&mut Foo = transmute(data);
foo.add(x as int);
println!("{} was the output", x as int);
};
let data = Foo::new();
unsafe { set_callback(r, &data as *const Foo as *const c_void); }
for i in range(0, 10) {
unsafe {
check(10, i);
}
}
// Now we must manually drop(data); and drop(r) here, othewise check will segfault.
// because data will already be dropped.
}
(source)
Having the C FFI interact with rust structures requires an explicit model of how the lifetime of rust structures that may cross the FFI boundary interact with the lifetime of the C representations of those structures. (In other words, both C and Rust need to have some agreement about the lifetimes of shared data structures.) At present, there is no way to explicitly enforce the relationship between the lifetimes of two representations of the same data structure, so that code like the above must rely on a deep understanding of Rust’s and C’s allocation semantics in order to work correctly. A linear type provides a means of documenting that variable lifetime has been explicitly considered:
extern {
fn set_callback(cb:|c_int|, state:*const c_void);
fn check(a:c_int, b:c_int);
}
fn main() {
let r = |x:c_int, data:*const c_void| {
let foo:&mut Foo = transmute(data);
foo.add(x as int);
println!("{} was the output", x as int);
};
let r |x:c_int, data:*const c_void| = Linear(r);
let data = Linear(Foo::new());
unsafe { set_callback(r, data as *const Foo as *const c_void); }
for i in range(0, 10) {
unsafe {
check(10, i);
}
}
// compilation will fail unless we manually drop(data); and drop(r) here.
// using linear types prevented a segfault.
//drop(r.deref_move());
//drop(data.deref_move());
}
Isn’t this just like sprinkling free() calls through the code?
Sort of, but it’s much safer than C’s free(). There are two major problems with explicit resource clean-up in C-like languages:
- Failure to free.
- Use after free.
This proposal continues to prevent both issues in rust:
- The obligation that data be moved out of a
lineartype means that it is impossible to fail to free resources (compilation will fail if thelinearvalue is not explicitly destructured for drop); AND - Rust’s borrow-checker continues to enforce that use-after-free is prevented.
This design is intended to bring back some benefits of explicit resource management, without inflicting their costs.
But linear types don’t interact well with unwinding?
The linear type as described here is not a true linear type: when unwinding past a linear type, the linear modifier is effectively dropped, so that the contained value will be dropped appropriately. Supporting unwinding means that Rust’s linear types would in effect still be affine. However, if we ever allow a post-1.0 subset of rust without unwinding, Rust’s linear types would become true linear types.
Further, unwinding should be extremely infrequent in rust code of any reasonable quality. As such, the linear types as presented in this proposal, while not truely linear, are probably within an epsilon of acting like true linear types in practice.
Detailed design
Add a linear attribute that can be applied to compound-type items. A variable of a type with a linear attribute behaves identically to variables without the linear attribute, except that such a variable cannot be dropped unless all contained items have been moved out of the variable. A non-linear container with a linear field cannot be dropped unless the linear field is moved out of the container.
This design has the following consequences:
- Only compound types can be linear.
- No fields in a linear type can be
Copy(though this can possibly be relaxed). - RFC #533 must be accepted.
- Certain generic items cannot be parameterized with linear types. (Of particular note,
std::mem::dropcannot be called with a linear type.) - Linear types cannot implement
Drop. - Linear types cannot be
Copy.
Further discussion of points 1 and 2 will be discussed under the Alternatives heading. Points 3 and 4 greatly affect the implementation, and will be further discussed below. Points 5 and 6 fall out naturally from the other considerations.
Before discussing points 3 and 4, I’d like to define some types that can be used as a basis for discussion:
#[linear]
struct Linear<T>(T);
impl<T> Linear<T> {
fn deref<'a>(&'a self) -> &'a T {
&((*self).0)
}
fn deref_mut<'a>(&'a mut self) -> &'a mut T {
&((*self).0)
}
fn deref_move(self) -> T {
let Linear(inner) = self;
inner
}
}
struct Base;
struct Base2;
#[linear]
struct LinearPair {
base1: Base,
base2: Base2,
}
Dropping variables of linear type.
A variable of linear type can be implicitly dropped when all fields from the linear type have been moved out. That is, the linear variable can be dropped when all of its fields have been partially dropped. For example:
fn drop_linear_base(lb: Linear<Base>) {
// partial move of `inner` from `lb` allows `lb` to be dropped.
let Linear(_) = lb;
}
fn drop_linear_pair(lp: LinearPair) {
// both fields of `lp` must be dropped to allow `lp` to be dropped.
drop(lp.base1);
drop(lp.base2);
}
On the other hand, the following code would cause compilation errors:
fn drop_linear_base_fail(lb: Linear<Base>) {
// generates compilation error:
// error: attempt to drop non-empty linear variable `lb`.
}
fn drop_linear_pair_fail(lp: LinearPair) {
// generates compilation error:
// error: attempt to drop non-empty linear variable `lp`.
drop(lp.base1);
// errors because only *one* of the fields from the linear type has
// been dropped.
}
This restriction also means that conditional drops of fields from the linear type are disallowed: A field must be unambiguously dropped, or not dropped, at every merge point. Taking inspiration from the notation in RFC #210:
struct S;
fn test() -> bool { ... }
fn f1(lp: LinearPair) {
// LINEAR OBJECT STATE
// ------------------------
// {lp.base1: owned, lp.base2: owned}
if test() {
drop(lp.base1);
// {lp.base1: dropped, lp.base2: owned}
} else {
drop(lp.base2);
// {lp.base1: owned, lp.base2: dropped}
}
// MERGE POINT: linear object state must match on all incoming
// control-flow paths. That it does *not* match here means that
// an attempt to compile this function should result in a
// compilation failure.
}
Dropping containers with linear fields.
A container with linear fields can be dropped if all linear fields have been moved out of the container. This enforces the linear restriction that the linear field must be explicitly moved. There are a few cases to consider:
- The container is
Copy.
We disallow this case by construction: By disallowing allow linear types from being Copy, we prevent structs containing linear fields from being Copy.
#[linear]
// this struct definition will cause a compilation error:
// error: the trait `Copy` may not be implemented for this type; etc.
#[derive(Copy)]
struct CopyFoo(LinearBase);
// this type definition will cause a compilation error:
// error: this type cannot be simultaneously `linear` and `Copy`.
#[linear]
#[derive(Copy)]
struct Bar(i32);
- The container is
Linear.
This has no special case handling: The already described rules for allowing drops of linear types cover this case.
- The container does not implement
Drop.
This case falls out naturally from what has been so-far described: The linear fields must be partially moved from the container in order for the container to be dropped.
struct PartialDropContainer {
lb: Linear<Base>,
}
void partial_drop_container_1() {
let mut x: PartialDropContainer;
// x can be dropped: no fields have been moved in.
}
void partial_drop_container_2() {
let x = PartialDropContainer { lb: Linear(Base) };
// must drop the linear field explicitly in order to allow the container
// to be dropped.
std::mem::drop(x.lb.deref_move());
}
- The container does implement
Drop.
This case currently will not work in an ergonomic way, because rust does not allow partial moves from types that implement Drop, even during the drop call. This strikes me as overly restrictive: it should be possible for rust to know which fields have been partially moved from the container by the end of the drop call, and handle the case appropriately. Details remain to be worked out, but code like the following can technically be made to work in a safe way:
struct AffineOfLinear(Linear<Base>);
impl Drop for AffineOfLinear {
// special `&drop` pointer type added for sake of illustration.
// alternative ideas are welcome.
fn drop(&drop self) {
// partial move out of `self`, currently disallowed.
let AffineOfLinear(inner) = self;
std::mem::drop(inner.deref_move());
}
}
There could be other benefits to allowing partial moves during drop execution (for example, it would be possible to maintain a Vec<> of all contained fields that had been dropped, perhaps for logging purposes). The current behavior seems more restrictive than necessary, to me.
Restrictions on generic functions.
Since linear types cannot be implicitly dropped, any generic function which includes implicit drops on an arbitrarily-typed variable must fail to compile when parametrized with such a variable of linear type. In other words, functions such as std::mem::drop should not accept variables of linear type.
There are two ways that this restriction could be enforced:
- By explicitly modifying the generic parameter list, to indicate whether a type parameter is allowed to be linear.
- By inferring from the function implementation whether the type parameter is allowed to be linear.
Though explicit notation is easier to describe, its usefulness is better demonstrated when type-parameter inference can break down, so I will describe the inference method first.
Inferring whether a type parameter can be linear.
Generic functions
The compiler can determine if a type-parameter to a generic function is allowed to be linear by analyzing the code implementing that function: if any variables of that type get moved or dropped in a way that is inconsistent with a linear type, then the compiler will be able to infer that the type-parameter should be !Linear. For example, in the current implementation of drop:
pub fn drop<T>(_x: T) { }
Because the _x argument receives a move into function scope, and is implicitly dropped on scope exit, the T argument to the drop routine can be inferred to be !Linear. Likewise:
fn drop_wrapper<T>(x: T) { drop(x); }
In this case, because the argument to drop cannot be linear, the x argument to drop_wrapper cannot be linear.
Generic traits
There should generally be no problem with unspecified constraints on types in generic traits: The compiler will default to the most permissive implementation, and allow either linear or non-linear types to be used as type parameters for the trait. If there is a problem in using a linear type as a type-parameter to a generic trait, this should show up in the attempt to implement the trait for a structure. For example, consider the following:
trait Consumer<T> {
fn consume(&mut self, t: T) { std::mem::drop(t); }
}
Here, the default implementation of Consumer::consume behaves equivalently to drop. An attempt to define this trait against a linear type will fail to compile. On the other hand, this should compile successfully (although the behavior may not be desirable):
trait Consumer<T> {
fn consume(&mut self, t: T) { std::mem::drop(t); }
}
struct Container {
lb: Linear<Base>,
}
impl Consumer<Linear<Base>> for Container {
fn consume(&mut self, lb: Linear<Base>) {
unsafe {
std::ptr::write(&self.lb, lb);
}
}
}
Since the lb argument was moved in the implementation, the function does not violate the linear type restrictions, and is allowed to compile. (This sort of facility can be used to define a Vec implementation containing variables of linear type. Note that the existing Vec cannot apply to linear types, as its Drop implementation violates the linear type restrictions.)
Generic structures and enums
A type-parameter for a generic struct or enum allows linear types only if all functions defined in the crate for the struct or enum type do not violate the linear type restrictions.
This has important knock-on effects for API design. For example, the current Option<T>::unwrap_or function implementation (reproduced below, with annotations) would prevent Option from wrapping linear
types.
unwrap_or(self, def: T) -> T {
// both `self` and `def` are moved into this function scope.
// if `self` is `Some`, the linear type field must be
// moved out before `self` can be consumed (which happens).
// but because `def` would also be linear, def must also be
// moved out for this function to by applicable to linear
// types.
match self {
Some(x) => {
// x is properly moved out, `self` can be consumed,
// but `def` will be implicitly consumed in this
// branch, so that the compiler will infer that
// `Option<T>` cannot be applied to linear types.
x
},
None => def
}
}
A proposed solution to this issue will be discussed below.
Explicit type parameter annotation.
The ‘?’ sigil in type parameters is currently used with the Sized kind to denote whether an unsized type can be used as a type parameter (with the assumption that, by default, only sized types should be
usable as type parameters). In this proposal, we add a Linear kind to denote whether a linear type can be used as a type parameter (with the assumption that, by default, the linearity of the type parameter will be inferred). Since kind inference can only be successful against function implementations, an explicit type-parameter annotation would allow kinds to be restricted for traits, structs, and enum type-parameters, as well. Further, an explicit annotation will allow users to notice if they have written code with the intention that it allow a linear parameter, while a bug in the code causes the compiler to infer that the type cannot be linear.
I also propose extending the impl for syntax so that one can have multiple (non-overlapping) impls for different kinds of type parameters.
?Linear
The ?Linear kind annotation will enforce that a type-parameter be allowed to be linear. When applied to a function item, it will result in a compilation error if the inferred kind does not allow a linear argument:
// will cause a compilation error: parameter `t` of linear type `T`
// cannot be implicitly dropped.
fn my_drop<T: ?Linear>(t: T) {
}
// allowed.
fn my_id<T: ?Linear>(t: t) -> T {
t
}
(This same behavior would also apply to default implementations of trait functions.)
impl for extension.
As mentioned above, the semantics proposed in this RFC would currently prevent Option<T> from being parameterized with a linear type. To ameliorate this issue, I propose to extend the trait for and impl for syntax to allow non-overlapping interfaces to be specified for a type based on the kind of the type-parameter. To motivate the discussion, we’ll consider how to modify Option<T> to allow it to wrap a linear type.
Most of the routines defined in the impl<T> for Option<T> are allowable whether Option wraps a linear type or not:
impl<T: ?Linear> Option<T> {
pub fn is_some ...
pub fn is_none ...
pub fn as_ref ...
pub fn as_mut ...
pub fn as_mut_slice ...
pub fn expect ...
pub fn unwrap ...
pub fn map ...
...etc...
}
However some can only be applied when the type-parameter is not Linear:
impl<T: !Linear> Option<T> {
pub fn unwrap_or ...
pub fn unwrap_or_else ...
pub fn map_or ...
...etc...
}
If Option is parameterized with a Linear type, the routines specified in the impl<T: !Linear> will not be available to callers. Similarly, a ~Linear restriction would mean that only Linear types can have access to the named interfaces.
A similar idea can be applied to trait for syntax:
// denotes that the trait interface will be available no matter whether the
// type the trait is bound to is linear or not.
trait Foo for ?Linear {
}
// these trait interfaces will only be available when the trait is
// bound to a non-linear type.
trait Bar for !Linear {
}
// these trait interfaces will only be available when the trait is
// bound to a linear type.
trait Baz for ~Linear {
}
Drawbacks
Overall, this proposes a significant change to the language, and there are several pieces required to make linear types usable. Where new facilities felt necessary to improve the ergonomics of working with linear types (&drop references, kinded impls), I’ve attempted to make those facilities more broadly useful, so that it would be useful and meaningful to fold aspects of this proposal into the language as parts.
Some aspects of this proposal push for change in some APIs. All such changes would be backwards compatible, at least at a source level (I am not familiar with rust’s .rlib binary representation), however the utility of many parts of the standard library (and other libraries) would be improved under this proposal by separating those interfaces which can apply to all type-parameter kinds, from those that can only apply to non-linear kinds. (The text mentioned Option<T> explicitly. Another type which might have the same concerns is Vec<T>.) This would cause some churn in library implementations, but the modifications would generally be highly mechanical. (Refactoring the impl<T> Option<T> was perhaps the easiest part of this RFC to write.)
Alternatives.
Do nothing.
We could not do this, and live with the status quo. I tried to show why this is disadvantageous in the Motivation above, but it is probably not a show-stopping issue. However it strikes me as unlikely that “eager drop” will be usable unless there is some way to remind users that their variable lifetime may not be what they expect it to be.
Allow non-compound linear types (i.e. type aliases, or empty types).
In this proposal, only compound types can be linear. This is necessitated by the means described of allowing linear variables to be dropped (by moving all contained fields from the linear container). An alternative design would allow the #[linear] attribute to be applied to non-compound types (such as type aliases), and have the attribute be non-effectual in those cases (that is, the resulting type would not have any additional restrictions on drop behavior). A lint could check if a #[linear] attribute were applied to a non-compound type, with default behavior set to warning or error.
I believe this would be inferior to the more clear rule that linear types must be compound. By applying the #[linear] attribute to a type a developer has directly signaled that the type should have restrictions placed on dropping. Simultaneously asking for such a restriction, and preventing the compiler from enforcing that restriction, is a logical inconsistency that should unconditionally be reported as an error.
Allow Copy fields as linear elements.
If a field is Copy, it cannot be moved from the linear variables, which would prevent the linear destruction mechanism described above. An alternative design would be to allow linear variable destruction when all Move fields are moved from the structure, but this seems undesirable for the same reasons described above.
Unresolved questions
None that I can think of.