RFC: Add linear type facility

[pnkfelix]

Rendered

Tracking issue for postponed PR #776

[mzabaluev]

This may be useful to support close methods for I/O objects that need error reporting when being disposed of. See a discussion thread on I/O issues.

[Munksgaard]

Are there any plans for when we take this up again?

523 seems to be related, by the way.

[aidancully]

@Munksgaard I've factored some of this RFC out into #1180, and (opened a discussion on internals about another part)[https://internals.rust-lang.org/t/pre-rfc-excdrop-trait-for-different-drop-glue-during-unwinding/2242]. I've been working through an implementation of #1180, but real life is taking too much time to make any progress at all for probably the next month or so.

[Rufflewind]

Aside from fallible Drop constructors (e.g. closing a file), there’s another situation where it could come in handy: Sometimes an resource is held by another thread/process/host and dropping would require waiting for for the other side to complete whatever they are doing. Implicit drops would cause cause the program to block, possibly unintentionally (which can further lead to unintended deadlocks). Worse, the protocol might not even offer a way to wait for it, in which case there’s nothing you can do but panic. In these kinds of cases, it would have been better to have simply caught it as a compile error.

I think linear types are suited for transient, active things that need to be dealt with carefully and explicitly, whereas affine types are more like passive objects that could be thrown away without regard. Which one is more suitable for a particular resource is probably a bit subjective and dependent on the robustness and reliability demands.

It might even be possible to have a rudimentary lint-based implementation of linear types: if an object gets dropped and the destructor unconditionally panics, then that’s almost certainly a bug and should be warned.

[jethrogb]

It might even be possible to have a rudimentary lint-based implementation of linear types: if an object gets dropped and the destructor unconditionally panics, then that’s almost certainly a bug and should be warned.

How would that work? Presumably when people say linear types they don't mean types with values with an infinite lifetime, but rather that you need to pass them to some special destroy function by value when you're done with them. If you have a Drop impl that always panics you can't even do this (safely).

[Rufflewind]

How would that work? Presumably when people say linear types they don't mean types with values with an infinite lifetime, but rather that you need to pass them to some special destroy function by value when you're done with them.

It’s not infinitely long, but the time at which it becomes destructible is not statically known, and may require the user to take certain actions before it becomes destructible.

If you have a Drop impl that always panics you can't even do this (safely).

Yes, panicking in drop is really awkward, so I’m hoping linear types could help obviate the need for such workarounds.

[ghost]

It's been over 5 years now since this was postponed.

[carado]

6 years now, is this ever gonna be considered ? There have been a bunch of times when I've wanted something like this.

[Philonoist]

This is so important! If this would be supported, rust could be the primary language to compile to cairo bytecode...

[leviska]

Use cases:

1. Async drop. Instead of implementing async drop, you can forbid drop for the type and implement async fn method that must be called instead of dropping.
2. Drop with arguments. Imagine a handle, that is created from some resource manager and needs a reference to this manager on drop. One way is to store the reference inside the handle (which can be tricky/expensive with Arcs/Mutexes/etc.), but the other way is to make drop accept the reference to the resource manager. With this you can forbid drop and implement custom function that accepts additional arguments.
3. Drop that can fail/can have side effects. Again, the same idea, you can forbid drop and write a function, which will return error, for example, if drop failed, so it will be the job of the programmer to handle this error correctly

You can already write this functions and use them, but I think the biggest problem is that if you forget to call them, the compiler will place the default drop (and drops can be hidden in some function calls). And I understand that there is a big problem with handling this custom drops during panic, so may be add cheaty linear type:

Basically instead of just banning the drop, may be add an 'annotation' to the compiler, saying "do not add drop for this type during compilation; instead, throw compile error". So, an example:

{
    let a = Foo::new();
    // compiler 'will add' std::mem::drop(a);
}

Instead, if the type is annotated as "no drop", in this snippet compiler will just throw an error. This can help with cases 1 and 3: in async case, we can block in the drop; in the drop-can-fail case, we could just ignore an error (because it will be called only during panic and something already went wrong). And even in the second case some one can be fine with resources "leaking" from resource manager during panic.

I know this is an error prone way to do this, but it kinda doesn't violate rust rules. You can already write all that code (blocking, ignore an error, do nothing with custom resource manager) in safe rust, but yes, you shouldn't, and the lack of the no-drop kinda forces you to find a better way. But I think this "annotation" could help in a lot of cases, where there is just no better solution.

[Demindiro]

I've found that using must_use in combination with forbid(unused_must_use) is effective as a crappy form of linear types, e.g.:

#![forbid(unused_must_use)]

#[derive(Debug)]
#[must_use = "Must be manually destroyed with `T::destroy()`"]
struct T;

impl T {
    fn destroy(self) {
        std::mem::forget(self)
    }
}

impl Drop for T {
    fn drop(&mut self) {
        if !std::thread::panicking() {
            panic!("Must be destroyed with `T::destroy()`");
        }
    }
}

fn main() {
    dbg!(T);
}

error: unused `T` that must be used
  --> src/main.rs:22:5
   |
22 |     dbg!(T);
   |     ^^^^^^^
   |
   = note: Must be manually destroyed with `T::destroy()`

If you replace dbg!(T) with dbg!(T).destroy() it compiles and works as expected.

EDIT: in hindsight it doesn't work if you have e.g. f(&self) and call T.f(). Ah well

[SOF3]

Where does the word "linear" come from? Is there any prior work in other languages for reference?

[Kixiron]

Linear types are a form of substructural type systems, notable implementors are Clean and Haskell (via GHC extension)

[afetisov]

@SOF3 The word "linear" comes from the notion of linear logic. I believe the concept, and the terminology, were first proposed in a 1987 paper Linear Logic by J.-Y. Girard. The terminology was likely motivated by two related concepts, coming from the theory of vector spaces and linear operators. People often talk about "linear relations" or "linear terms" when variables occur only once in the formula, by analogy with linear functions, which have a single occurrence of each coordinate variable in their expression. In linear logic, an element of each type can be used only once in the formula, because construction of pairs (x1, x2): X \times X is forbidden for general types. Linear logic doesn't allow duplication of values (unless special operators are used). Similarly, linear logic doesn't allow silent discarding of values: if you have an element x: X, you must explicitly thread it through all formulas, and can't just "forget" to use it.

The second, more conceptual, reason to call this logic "linear" is that it arises as internal logic of the additive symmetric monoidal category of vector spaces. Basically it is the only way your logic could be structured if vector spaces were all you knew about, and it allows to prove all facts about them. The categorical model served as the guiding star for the formulation of logic, but for practical applications the later found model of resource semantics is much more relevant.

[aleokdev]

Any progress on this? What is it blocked on? This would be incredibly useful for interfacing with externally handled buffers, such as the ones present in a GPU. Other alternatives require having a device around to be able to destroy the resources, which unnecessarily adds bloat to the structure or to the global namespace.

I'd be willing to work on it if the PR gets considered.

[golddranks]

@aleokdev Unlikely to happen. I think @Gankra's blog post "The Pain Of Real Linear Types in Rust", that for some reason is not linked in this thread, killed the feature for many: https://faultlore.com/blah/linear-rust/