[pre-RFC] linear type modifier

[nodakai]

This idea is very interesting to me though I’m not sure if we really need a new type for it.

I also thought about a command line option for rustc to print out program locations where Drop::drop() are inserted before.

[eddyb]

I appreciate the detailed proposal, but I can’t agree with it.

First off, it requires a keyword. Those are pricey and we have reserved a bunch of them already like JS did, very wasteful IMO (I fear we’ll be forever stuck with the likes of be and override). If we replace linear T with Linear<T> or #[linear] T (though we don’t have support for the latter), this becomes more like #[must_use] with stronger semantics.

Even then, I’d have to argue that the usefulness of linear types which can be consumed at will without any restriction imposable by a type, is quite limited. Or that they’re not even linear types!

The drop function is defined as fn drop<T>(_: T) {}, par excellence affine, not linear. If drop(x) works, then let _ = x; and (unless #[must_use]) {x;} also work. Kind of reminds of the “noisy drop” discussions.

I have sketched my own linear type design, it was simpler to implement than this and it worked better for my usecases (specialized consumer functions) - but it wasn’t very well received so I shelved it. I’ll embed it here for future reference:

// std::markers:
#[lang="linear"]
struct Linear;
impl Linear {
    fn consume(self) { unsafe { std::mem::forget(self) } }
}
// std::thread:
struct Thread<T> {
    // ...
    linear_marker: markers::Linear
}
impl<T> Thread<T> {
    fn detach(self) {
        // This can only be done in std::thread because linear_marker
        // is private, and partial moves are disallowed.
        let {/*...*/, linear_marker} = self;
        // Dispose of the only reason self is linear.
        linear_marker.consume();
        /* detach thread etc. */
    }
    fn join(self) -> T {
        let {/*...*/, linear_marker} = self;
        // Dispose of the only reason self is linear.
        linear_marker.consume();
        /* join thread etc. */
    }
}

Since the kinds and related markers are going away (for Copy, Sync and Send) it may make more sense to use a Linear trait here (necessary in some form if you want to allow generics to opt-in to being instantiated with linear types - another important point this proposal doesn’t cover), and impl<T> Linear for Thread<T> in a similar way to Drop. I would then guess that having at least one private field will be the only requirement to restrict consuming a linear type to the module where it is defined (which can then provide a restricted interface, as it is the case with the rest of Rust’s abstraction-building primitives).

[glaebhoerl]

Conveniently, if &out T is never Send/Share, it would also be unwind-safe despite unwinds breaking linearity.

Could you elaborate? Is this the formulation where &out may only point into the stack?

[aidancully]

For what it’s worth, embedded developers often argue about whether it’s allowable to use dynamic memory allocation at all, precisely because of the likelihood of unexpected error. We live without access to large portions of the standard library… But we can’t work without provable bounds on resource usage.

[aidancully]

Thank you for the detailed feedback… I’m still working through it, and hope to address it more completely, later. It also occurred to me overnight that the way I’ve used drop in the proposal wouldn’t work for the reason you mention… In the spirit of the original proposal, I’d remove the implicit coercion from linear T to T, and add an explicit unlinearize transformation, so that you would need to drop(unlinearize(T)). (In an earlier draft, I did this with a DerefMove-type operation: you would need to drop(*foo). Probably that was the technically better choice.)

[eddyb]

That is an improvement, but it still doesn’t allow building abstractions like my Thread example above, File::close (this was given as an example on reddit a while ago, I believe) or &out pointers.

[aidancully]

Does this come closer to the spirit of what people would like to see?

#[linear]
#[deriving(Drop)]
pub struct Linear<T>(T);

impl<T> DerefMove<T> for Linear<T> {
    pub fn deref_move(self) -> T {
        let Linear(inner) = self;
        inner
    }
}

[kmcguire]

I have grown to like the automatic drop of resources with out explicitly dropping them. I feel like it is really ergonomic. This proposal does not really bother me until you commonly used libraries start doing it and then it will become annoying.

One specific case would be an existing code base requiring major overhaul because the developer of a library dependency thinks it would be a good idea to make a type linear. So now I wake up and have to go through tons of code fixing it because someone else thought I did not know what I was doing. So unless there is a way to turn it off I really do not like it.

Also, I do not know of many real world situations where I had a problem with automatic dropping. I am usually in tune with my work enough to have all potential factors in mind while I write code. In regard to the mutex example above. I have never had a problem with dropping of a mutex guard! I mean if you let that mutex guard drop out of scope while you still need it then you are:

1. Not paying good attention to what you are doing at all.

2. Should have been protecting the T in Mutex<T> not something outside of it, because otherwise you would be unable to access it if the guard drops. You basically have weak protection using the mutex to protection something outside of it.

Like I said the linear type sounds great as another feature but to summarize:

1. MutexGuard<T> does not need to be explicitly dropped.
2. A linear type can get annoying very quickly even though the library author thinks it is a good idea.
3. No proposed way to turn it off, or make it a warning, or something less devastating than an error.
4. It complicates rustc which means it consumes more programmer fuel each time something is changed or fixed. That is one more part on an ever increasing complexity we call rustc. Is it worth it? Likely not.

[aidancully]

For what it’s worth, I’m working on a new version of this proposal that allows a Drop wrapper around a linear type. It’ll take a little more time before it’s ready to post, but it would allow one to write an affine wrapper around a linear type:

struct Foo;

#[linear]
struct LinearFoo(Foo);
fn explicit_cleanup_function(lf: LinearFoo) {
  ...
}

struct AffineOfLinear(LinearFoo);
impl Drop for AffineOfLinear {
  fn drop(&mut self) {
    let AffineOfLinear(inner) = self;
    explicit_cleanup_function(inner);
  }
}

In this case, even if your library author made a bad choice, it’d be possible for you to put a wrapper around his linear type allowing it to be treated as affine. Still, part of choosing a library is evaluating its ergonomics, and comparing the author’s development philosophy to yours… If they disagree too much, there will almost certainly be some pain in relying on that library. If they generally agree, that author is less likely to make a choice that hurts.

Importantly for me, I know of cases where implicit drop of a variable would absolutely be a program error (involving intrusive structures), and linear types feel like the solution in those cases. As a separate argument, I think “eager drop” is likely to prove difficult to use without a linear type facility…

[jroesch]

don’t really understand any of it

In Intutionistic Logic there are 3 rules referred to as the “structural rules” if you drop any of these rules you find your self in a substructural logic (i.e affine, linear, relevant, ordered). Which rules you choose to drop give you different logics and therefore different type systems.

You get relevant by dropping the weakening rule, a rule that allows you to have unneeded assumptions when performing a proof, so as a programmer this means we have to use every term (everything is “relevant”).

You get a affine type system by dropping contraction, the rule that allows you to duplicate an assumption an arbitrary number of times, this means every value can be used at most once.

You get linear by dropping both weakening and contraction meaning every value must be used exactly once.

Finally you can get an ordered type system by dropping the exchange property which allows the you to reorder assumptions arbitrarily. Removing this rule means as a programmer you must use terms in the order they are introduced, restricting programs even more.

Here is a high level overview from Wikipedia: http://en.wikipedia.org/wiki/Substructural_type_system

The metatheory can be a little complicated but the ideas are simple.

[aidancully]

Second pass at a linear types RFC is here.

[Ericson2314]

@glaebhoerl Thanks, I had forgotten about heap allocated &outs, but it in fact works out. The &out to heap does not own the box, just the contents of the box, so to speak. Unwinding will hit the &out T, and do nothing, and then hit the borrowed Box<T>. The lack of Send+Sync ensures the box and &out will never be unwound separately.

[glaebhoerl]

My assumption was that unwinding would hit the Box<T>, which would invoke the destructor of T, which would segfault because it is in an uninitialized state. How would it “know not to”?

(Hence my working assumption has been that the only way to solve this problem in general is for unwinding through an &out to abort - and that this is still worth it. It may be possible to have special-case solutions which avoid the abort, like tying it to Default (or a separate Init trait) which works like the opposite of Drop, and reinitializes the referent of the &out when unwinding hits it.)

[Ericson2314]

Well this compiles http://is.gd/iOLJc2 . So either the problem is solved, or we already have it.

[glaebhoerl]

If I’m not misinterpreting your example, then here it’s the stack-allocated Box variable x which is uninitialized. The problematic case would be if the heap-allocated contents of the Box, *x, were uninitialized when unwinding hit it. The compiler has static knowledge of the former, but not the latter. As far as I know there’s no way currently to bring about the second scenario (which is a good thing).

[Ericson2314]

You are right the example is not good enough. Whether or not a box is /borrowed/ is a statically analyzable however. IIRC there are plans to make it so one can move out of a &mut as long as something is moved back in, like http://is.gd/cZxiQ6 (which does not currently compile). borrowing a &out should be no different. Either of these would just require a drop flag in some circumstances.

[glaebhoerl]

Yeah, moving out of an &mut conceptually leaves you with an &out.

How could main / Box know in this scenario whether or not *x is initialized? How do you envision the drop flag working? (Where would it go, who would set it?)

I also want things like:

fn emplace_back<'a, T>(vec: &'a mut Vec<T>) -> &'a out T

where it’s only the last element in the Vec that’s uninitialized until the &out obligation is fulfilled.

And:

fn emplace_back_n<'a, T>(vec: &'a mut Vec<T>, num: usize) -> &'a out [T]

here the number of uninitialized elements depends on a runtime value.

It seems like these would require quite sophisticated drop flaggery to tolerate unwinding - likely at an unacceptable performance cost…

[Ericson2314]

The idea is &out can only be eliminated by assignment, in which case you are left with a &mut. If you move it (technically re-borrow and move it) and don’t end up with something with the same lifetime, it must have been written to. That means if you pass &out to a function that returns unit, lets say, the &out becomes a &mut just as if you assigned it yourself.

From an unwinding perspective, the basic thing one needs to know is whether something is borrowed, which is a statically analyzable property. I hope then that in all non-array cases the needed is-borrowed state could somehow be hard coded into the dwarf metadata so as not to occur any overhead unless panicking occurs. In normal operation, the &out must be eliminated before the borrowed thing is dropped, so actually I don’t think a drop flag is needed ever. Note that the same thing could be done for &muts, with mut-borrowed slots never running destructors and unborrowed &muts running them instead, though there is probably no reason to do this other than consistency with &out.

The array case is more complex as you say. Note that a Vec already tracks capacity vs length. It may be sufficient then to wrap the &out ptr in something which will bump the capacity on assignment as a side effect.

Granted this a bit of a cop-out out answer – Vec relies on yet another unsafe implementation detail, and the uninitiated values must be contiguous and at the end.

An interesting thing to note is that it is not allowed to refine an &out with a .field. One would need to pattern match to get an &out to each field of the struct/variant if one wants to fulfill each assign obligation separately – let &out (ref a, ref b) = some_out;. Fine grained borrowing would work on [T; n] more easily than [T], precisely because the former can be pattern matched so much more “thoroughly”.

[glaebhoerl]

The borrow checker knows nothing about the structure of heap-allocated data structures. Box is very simple and contains a single value, but you could take out an &out borrow of a single element of an arbitrary complex dynamic structure (HashMap, BTreeMap, …?). How does it know, when unwinding, which element has (or hasn’t) been &out-borrowed? From a borrow checker perspective, if you do foo.get_out_borrow_of_element(bar, baz), I think all that it’s aware of is that foo has been &mut-borrowed. But that’s not nearly enough information.

If you’ve directly &out borrowed something directly visible to the borrow checker on the stack, in that case it could know not to re-run the destructor - but at the inner function where the &out itself is live, you can’t know whether this the case, and where it’s been borrowed from… (and hence, whether it’s safe to let unwinding keep going).

(With respect to refining and &out [T] and so on you might be interested in this comment I made on the RFC a long time ago.)

[kvark]

Where can I find more info about your proposal and the reasons it was rejected? I find it pretty efficient.