Please view my example.
A fn<T>(&mut T, &mut T) accepts a &mut X and a &mut Y despite invariance.
Your example very explicitly says to any reader that scopes have, somehow, affect lifetimes. They had no direct relation to each other for years.
I don't understand
lifetimes are not tied to lexical scopes any more, this is called non-lexical-lifetime, that's what the linked documentation is about.
lifetimes are "regions" in the source code of borrows, which are inferred based on the code. here's a old but still relevant article on this topic:
also recommend to watch:
1 Like
Before we look at the example, let's cover some common misconceptions.
It has already been mentioned that Rust lifetimes -- those '_ things -- do not correspond to lexical scopes. Unfortunately a lot of learning material, including the official sources, tries to convey the gist of borrow checking by using analogies with lexical scopes. Or even -- incorrectly -- saying that lifetimes correspond to lexical scopes, or that lexical scopes denote Rust lifetimes. They do not.
Rust lifetimes -- those '_ things -- do not directly correspond to the liveness of of variables or other values, either. Instead, they generally correspond to the duration of a borrow of some variable or other place.
There are interactions between these things. It is an error for a variable which is borrowed to go out of scope, for example. But they are not the same thing, despite the unfortunate overlap in terminology.
At a high level, the borrow checker determines what places[1] are borrowed in what parts of your code,[2] and then checks every use of every place to see if there are any conflicts (such as moving or overwriting a variable which is borrowed). The duration of borrows is determined by where and how values that hold those borrows -- most commonly references -- are used.
The borrow checker also proves that any lifetime constraints -- e.g. due to function signatures or type annotations -- can be met. For example:
fn example(x: X) -> &'static str {
// call this `&'s str`
let y: &str = ...;
// This requires that `'s: 'static`. If the compiler cannot prove that it
// is possible to satisfy that constraint, it will emit an error.
y
}
In this respect, the borrow checker can be considered a constraint solver. Note that it doesn't need to choose exact durations for borrows -- it does not need to assign concrete lifetimes. It needs only prove that a solution to the constraints exists.
This part of borrow checking is what your playground is about IMO. Variance does inform these constraints.
Now let me walk through the example.
// 'outer scope
let numA = 1;
{ // 'inner scope
let numB = 2;
// 'refr scope
let mut refA = &numA; // Ref<'outer, i32>
let mut refB = &numB; // Ref<'inner, i32>
Lexical scopes do not correspond to lifetimes.[3] The declaration order of refA and refB don't matter either. It's too misleading to call these 'outer and 'inner, so I will call them:
let mut refA = &numA; // Ref<'n_a, i32>
let mut refB = &numB; // Ref<'n_b, i32>
You say...
// notation: "subtype € supertype"
// 'outer € 'inner
// Ref<'outer, i32> € Ref<'inner, i32>
...but up through this point in the code, there is nothing causing the lifetimes to be related. That said, something will cause them to be related later in the code. But you seem to think the scope of numA and numB is causing the lifetimes to be related (and thus that there is a subtype relationship due to the scopes). This is not the case.
Instead what the lifetime ends up "being" will be inferred from how refA and refB are used.
let mutA = &mut refA; // Mut<'refr, Ref<'outer, i32>>
let mutB = &mut refB; // Mut<'refr, Ref<'inner, i32>>
Nothing is causing the lifetime on the &mut/first Mut<..> parameter to be the same between these two variables either. Let's relabel them:
let mutA = &mut refA; // Mut<'refr_a, Ref<'n_a, i32>>
let mutB = &mut refB; // Mut<'refr_b, Ref<'n_b, i32>>
Due to invariance, it is the case that the lifetimes in the Ref<..> are 'n_a and 'n_b exactly -- the lifetimes from the types of the refA and refB variables.
func(mutA, mutB);
Here is the only code which causes any of the lifetimes above to be related to each other. This requires that you pass in two values of the same type. Let's call it Mut<'x, Ref<'y, i32>>.
Due to a mechanism called reborrowing, it need not be the case that 'refr_a and 'refr_b are exactly 'x. They need only be at least as long as 'x. So the call introduces the following constraints:
'repr_a: 'x
'repr_b: 'x
In Mut<'x, Ref<'y, i32>>, Ref<'y, i32> is invariant. The constraints in this case are:
'n_a: 'y, 'y: 'n_a // => 'n_a == 'y
'n_b: 'y, 'y: 'n_b // => 'n_b == 'y
So 'n_a == 'y and 'n_b == 'y. From this we can conclude that refA and refB have the same type -- that the lifetimes in their type must be the same.[4]
(The exact same type, not 'inner and 'outer with a subtyping relationship.)
dbg!(*mutA, *mutB);
This demonstrates that *mutA and *mutB were reborrowed in the call to func and not moved, or mutA and mutB would not be usable. It is also the last piece of code that contributes to any of the borrows staying alive. References don't have destructors, so the references going out of scope doesn't keep their borrows alive.[5] You can consider all of the borrows to end immediately following this point.
Nothing prevents the borrow checker from proving the constraints implied by the program, and there were no uses of places that conflicted with being borrowed. The program passes borrow check and compiles.
11 Likes
Once again, great, in-depth answer. I believe this is the third time you've helped me on this forum -- always regarding lifetimes -- and I'm always happy about the clarity and brainstorming-alongishness of your replies.
2 Likes
What confuses me about the video is the distinction between '0 and '1 at 12:13. Perhaps the '0 is just written at a misleading place.
To me, &'1 x makes sense. Admittedly, calling this '0 instead of '1 would have been more logical, since x is initialised at line 0.
&'0 u32 is where it gets confusing. Surely, the type of y is the same type as the type assigned to y.
If I'm not mistaken, this '0 represents something differently than the 'liveliness' of y as a variable, right? Earlier in the video, a distinction was made between live variables and live loans. Since y in itself is a variable, I'll assume that this '0 has something to do with the live of the loan of x, and not with y itself.
Due to variance, it doesn't have to be. Consider:
let local = 1;
// r1: &'a i32
let r1 = &local;
// r2: &'b i32; constraint: 'a: 'b
let r2 = r1;
println!(r2);
// 'b can end here (be no longer alive)
println!(r1);
// 'a can end here
The two types don't have to be the same.[1]
And the same is true here...
let y = &x;
// let y: &'0 u32 = &'1 x
...even though there is no longer an intermediate variable, the type of the &x expression need not be exactly the same as the type of the variable y.
Additionally, even when it ends up that the types must be the same (due to invariance say), the compiler can still use separate inference variables for the expression and the variable type. They'll just end up being constrained to be the same.
When walking through examples it's usually simpler to pretend the lifetimes are the same from the start, especially when it's something like this temporary &'1 x which is never going to end up being used anywhere except the assignment. So it might as well be '0 in this simple example. But behind the scenes there are inference variables like '1 all over the place.
I guess what confuses me is the distinction between the lifes for: x, y, '0, and &'1 x. Which of these are not necessarily the same thing?
If I understand correctly based on what you typed and what the speaker is saying, '0 (in the video) is equivalent to the life of y as a variable/path.
When I have:
1| let a = 12;
2| let r;
3| r = &a;
4| let b = 13;
5| r = &b;
6| print(r);
What lifetimes are at play, what loans are at play, what lifes are at play?
Well, the scopes of variables x and y aren't directly associated with (Rust, '_) lifetimes. And there is no lifetime in the type of x. There is a lifetime in the type of y -- that's '0. For simple examples, different inferred lifetimes -- especially those caused by a simple assignment like in the video example -- do end up being the same. In the example, '1 and '0 end up being the same. And the loan of x -- which is considered something distinct -- also ends up being the same.
In this simple example, I agree that it is hard to see the motivation for using different lifetimes, and having a distinction between loans and lifetimes.
An aside about the "lives of x and y"
Perhaps by "life of x, y" you meant their liveness locations, or their lexical/drop scope. The liveness of values whose types contain lifetimes are relevant to borrow checking, like the video walks through. If the type does not (like the type of x), it does not. And going out of scope isn't a lifetime, it's a use -- x becomes uninitialized when it goes out of scope, for example -- and it would be an error for x to be borrowed when this happens.
In practical terms, going out of scope can limit the acceptable lifetimes, because going out of scope conflicts with being borrowed. But being moved or having a &mut _ taken also conflicts with being borrowed. Due to the terminology and what most learning material is like, it is common to associate something going out of scope with the lifetime of some borrow, even if they don't think of moves or taking &mut _s the same why. Personally I find that to be more confusing than instructive. Instead I think of going out of scope as just another use -- one of many -- that may conflict with being borrowed.
The liveness of variables (with lifetimes in their types) does matter, but honestly, about the only time I think about it is when walking through how the borrow checker works. It isn't the only determining factor, as we'll see shortly.
So let's try another example to see the motivation:
fn main() {
let mut s1 = String::new(); // @1
let mut s2 = String::new(); // @2
let mut r = &mut s1; // @3: let mut r: &'0 mut _ = &'1 mut s1;
s2.push('H'); // @4
r.push('h'); // @5
r = &mut s2; // @6: r /* : &'0 mut _ */ = &'2 mut s2;
s1.push('i'); // @7
r.push('I'); // @8
} // @9
This compiles.[1] Walking through like the video does: r is used on @5, overwritten on @6, and used on @8. So '0 must include { @4, @5, @7, @8 }. But since this compiles, we can conclude that s2 is not borrowed on @4 and s1 is not borrowed on @7. Thus the loans of s1 and s2 must not be the same as '0.
I'll walk through your other code below to try to explain why, but I hope this makes the motivation for the allowing these lifetimes or loans to have different durations more clear.
In the video example, the liveness[2] of y ended up corresponding to the lifetime '0 in its type, and that's not uncommon for references you don't pass anywhere. So let's see something more complicated:
fn main() {
let s = "Hello, world!".to_owned(); // @1
let r = &*s; // @2: &'0 str = &'1 ...
let mut iter = r.split_whitespace(); // @3: Split<'2> = ...
let word = iter.next().unwrap(); // @4: &'3 str = ...
let moved_s = s; // @5
println!("{word}"); // @6
} // @7
This throws an error on @5 for moving s while it is borrowed.
What's the liveness of r? It's just { @3 }. But there's a big chain of lifetime constraints going on here such that '1: '0: ... : '2: ... : '3.[3] So '0 ends up being { @3, @4, @5, @6 }. In this case, the lifetime in the type of r contains more than the liveness of r.
(There are actually a lot more lifetimes present in the right hand side of the assignments than the ones I annotated, but it would be a distraction to try to track them all.)
To fully explain this new example (where you overwrite references), we'll have to go a bit deeper into how the borrow checker works. I'll be explaining in NLL terms, as that's what I'm most accustomed to explaining.
There are two loans: One of a and one of b. And there are three lifetimes we care about: Those for the borrow expressions &a and &b, and the lifetime in the type of r.
{
let a = 12; // @1
// @2
let mut r; // @3 Let's call the type of `r` &'r i32
// @4
r = &a; // @5 Let's call the type of the borrow expr. &'a i32
// @6
let b = 13; // @7
// @8
r = &b; // @9 Let's call the type of the borrow expr. &'b i32
// @10
print(r); // @11
// @12
} // @13
Recall from the video that lifetimes are calculated in part based on when variables with lifetimes in their type are alive. When is r alive? It is overwritten on @9, so it is not alive on @6, @7, or @8. It's alive on @10 and @11 due to the use on @11. And it's not alive after that as there are no more uses. (It does go out of scope on @13, but references have no destructor, and going out of scope does not keep their lifetime alive.)
So we can conclude that 'r includes { @10, @11 }.[4]
Let's look at b and 'b next. When are any variables with 'b in their type alive? There are none! However, the assignment of &b to r imposes a 'b: 'r constraint. That means that anywhere 'r is alive, 'b is also alive.[5] So 'b includes { @10, @11 } as well.
How about the loan of b? The loan is a shared loan and it is associated with the lifetime 'b. In this case, nothing interesting happens between the creation of the loan and the end of 'b, and the loan of b also ends up being { @10, @11 }. And indeed, if we try to modify or overwrite b on @10, we get a borrow check error.
The situation with a and 'a is similar in that there are no uses of 'a directly, but there is an 'a: 'r constraint, so 'a includes { @10, @11 }. And the shared loan of a is associated to the lifetime 'a. However, this is where the distinction between loans and lifetimes comes in to play: on any given control flow path, if 'a ceases to be alive, the loan doesn't include the parts of 'a along the rest of that path.
How the NLL RFC phrases it
For a statement at point P in the graph, we define the “transfer function” – that is, which loans it brings into or out of scope – as follows:
- any loans whose region does not include P are killed;
- if this is a borrow statement, the corresponding loan is generated;
- if this is an assignment lv = , then any loan for some path P of which lv is a prefix is killed.
("Region" is another term for "[Rust] lifetime".)
The reason is to be more flexible in the face of things like overwriting references.
The path after the creation of the loan is @6, @7, @8, etc. 'a is not alive on @6. So the loan of a in this case ends up being the empty set.[6] In contrast with b above, we can modify a on @6 and @10 and it's not an error.
So we've ended up with a loan which has a duration that is not the same as the lifetime in the type of the borrow expression that created that loan.
Going back to an earlier example:
fn main() {
let mut s1 = String::new(); // @1
let mut s2 = String::new(); // @2
let mut r = &mut s1; // @3: let mut r: &'0 mut _ = &'1 mut s1;
s2.push('H'); // @4
r.push('h'); // @5
r = &mut s2; // @6: r /* : &'0 mut _ */ = &'2 mut s2;
s1.push('i'); // @7
r.push('I'); // @8
} // @9
The loan of s1 doesn't include @7 because of the assignment on @6, similar to the example we just walked through. And the loan of s2 doesn't include @4 because loans propogate forward in the control flow graph, and the loan is only created on @6 (and there's no looping control flow to get back to @4).
(Does '2 contain { @4, @5 }, or is it omitted due to flow? In terms of implementation, I'm not actually sure... but I don't think it matters either way.)
On NLL, today; it doesn't require Polonius ↩︎
not the scope ↩︎
Uses of
wordkeep the borrow initeralive, which keeps the borrow inralive, which keeps the borrow ofsalive. ↩︎And some might say
@5and@9; but the NLL RFC doesn't. I think this is an implementation nuance and I'm not going to sweat it. ↩︎In NLL, and in lifetime insensitive Polonius, this subtyping relationship holds everywhere. In lifetime sensitive Polonius, the subtyping relationship is flow sensitive. However, that's irrelevant to this example. ↩︎
Note however that creating the borrow is a use of
athat can still introduce a borrow checker error, even if the corresponding loan would end up empty. If something else causedato be exclusively borrowed on@5, you would still get a borrow check error just for trying to create the&a. ↩︎
1 Like