well, I am learning subtyping rules of rust, and I am encountering the idea "Invariant". What I understood of "Invariant" is that : Given a generic type F, for a subtype Sub and its super type Super, F<Sub> is not subtype of F<Super> and F<Sub> is not super type of F<Sub> either. Only if when Sub == Super, F<Sub> == F<Super>. And I want a concrete example to validate my thought. And I try to write some codes.
The first case that I wrote is :
fn foo<'a: 'b, 'b>(x: &'a mut &'a i32, y: &'a mut &'b i32) {
*y = *x;
}
fn main() {
let a = 123;
{
let b = 134;
let mut a_r = &a;
let mut x = &mut a_r;
{
let mut b_r = &b;
let mut y = &mut b_r;
foo(x, y);
println!("{}", *x);
}
}
}
And it cannot be compiled which matches my thought.
But when I substitute foo(x, y) with *y = *x which is as following
fn foo<'a: 'b, 'b>(x: &'a mut &'a i32, y: &'a mut &'b i32) {
*y = *x;
}
fn main() {
let a = 123;
{
let b = 134;
let mut a_r = &a;
let mut x = &mut a_r;
{
let mut b_r = &b;
let mut y = &mut b_r;
// foo(x, y);
*y = *x;
println!("{}", *x);
}
}
}
It can be compiled now! why ? is there a special rule implemented for intra-function lifetime inference?
The problem is your signature forces lifetimes to be equal when they don't need to be. Here's the fix:
fn foo<'x, 'y>(x: &mut &'x i32, y: &mut &'y i32)
where
'x: 'y, // x's inner lifetime outlives y's inner lifetime
{
*y = *x;
}
fn main() {
let a = 123;
{
let b = 134;
let mut a_r = &a;
let mut x = &mut a_r;
{
let mut b_r = &b;
let mut y = &mut b_r;
foo(x, y); // Should compile (if I didn't get things wrong)
println!("{}", *x);
}
}
}
In your original signature fn foo<'a: 'b, 'b>(x: &'a mut &'a i32, y: &'a mut &'b i32)
&'a mut &'a i32 : ties the outer and inner lifetimes together
Both x and y have outer lifetime 'a tes them together too
This created an impossible constraint: the outer mutable borrow's lifetime had to equal a's lifetime, but it actually lives in a shorter scope. I can think of more simpler solutions, but I kept both the lifetimes because that's what you were talking about.
For completeness, and leaving this at dual lifetimes feels a bit bothersome to me :'D Here's what I would I actually write in this case. This works but hides the fact that the lifetimes don't need to be equal in this case, it implicitly implies that when only an outlives relationship is needed, both are forced to unify to the same (shorter) lifetime instead. Lifetimes was one of most annoying things for me for a long 'time'. I try to avoid complicating their usage whenever possible :'D
Intra-function lifetimes are determined by how borrows are used in the function body, and constraints imposed by things like the signatures of functions you call and type annotations in the function body. By inlining the body of foo, you removed some constraints that were required by the function signature.
There are some things allowed in function bodies that aren't expressible by function signatures, such as independently borrowing two fields of a struct.
Understanding the implications of lifetimes with regards to borrow check errors goes beyond just subtyping per se. Lifetimes also have implied bounds which can make things less obvious.
For example, let's look at the "lifetimes must be the same" case which @consistent-milk12 mentioned:
// When you have `&'a mut &'b i32`, it is implied that `'b: 'a`.
//
// (Otherwise you would have a reference to an invalid type/value, which
// is not allowed. It would be too tedious to have to write this explicitly
// everywhere you have a reference to something generic, so it's implied.)
//
// You added an explicit `'a: 'b`. Together with `'b: 'a`, this means
// that `'a` and `'b` must actually be the same lifetime.
fn foo<'a: 'b, 'b>(x: &'a mut &'a i32, y: &'a mut &'b i32) { ... }
This doesn't come up in the same way with non-lifetimes because there is no subtype bound for non-lifetimes. (There are associated type equality bounds, so maybe someone could cook up an example, but I can't recall ever seeing it happen accidentally in practice.)
On top of that, &'a mut &'a i32 means that the &'a i32 is borrowed forever. After the call to foo(x, y), none of x, y, a_r, or b_r are usable again. This does happen in part due to invariance,[1] but you also have to understand that equating the lifetimes meant keeping an exclusive borrow active for longer than you necessarily wanted to.
(I.e. we're talking about how borrow checking works, not just subtyping.)
I think practicing borrow checking is your actual goal, so let's look at the difference between the two other signatures for some more exercise. (If I'm wrong about your goal you may not care about this section of my reply.)
fn foo_2<'x: 'y, 'y>(x: &mut &'x i32, y: &mut &'y i32) {
*y = *x;
}
fn main() {
let mut a = 123;
let mut a_r = &a;
let x = &mut a_r;
{
let b = 134;
let mut b_r = &b;
let y = &mut b_r;
foo_2(x, y);
// This compiles.
println!("{}", x);
// This errors.
// a = 42;
// println!("{}", y);
}
// This compiles.
println!("{}", x);
}
With this signature, the important lifetimes are the inner lifetimes -- the lifetimes that correspond to the borrows of a and b. Those are the lifetimes which are invariant in the signature of foo_2. Let's say that a is borrowed for 'a[2] and b is borrowed for 'b.[3] And let's take a closer look at the call to foo_2.
// Let's say we called this with inner lifetimes `'x` and `'y`.
// (Like we called `foo_2::<'x, 'y>`.)
//
// Due to invariance, this is only possible if:
// - `'x = 'a`
// - `'y = 'b`
//
// And because `'x: 'y` was required, we must have `'a: 'b`.
//
// That means uses of `y` or `b_r` will keep `a` borrowed:
// `'a` must be active everywhere `'b` is active (and uses of
// `y` and `b_r` keep `'b` active). That is the meaning of `'a: 'b`.
foo_2(x, y);
This explains why uncommenting these lines results in an error:
// The use of `y` keeps `a` borrowed, and it is not allowed to
// overwrite something which is borrowed.
a = 42;
println!("{}", y);
And this is a good thing! *y is now a copy of a_r. So long as y is valid, you can pull another copy of a_r out of *y. a_r and all the copies of a_r are shared references to a, and it is undefined behavior for a to be altered while such shared references are valid.
fn foo_1<'f>(x: &mut &'f i32, y: &mut &'f i32) {
*y = *x;
}
fn main() {
let a = 123;
let mut a_r = &a;
let x = &mut a_r;
{
let b = 134;
let mut b_r = &b;
let y = &mut b_r;
foo_2(x, y);
// This compiles.
println!("{}", x);
}
// This errors.
println!("{}", x);
}
And to highlight the difference from foo_2:
// Let's say we called this with inner lifetimes `'f`.
// Due to invariance, this is only possible if:
// - `'f = 'a`
// - `'f = 'b`
// - and thus `'a = 'b` -- i.e. `'a: 'b` and `'b: 'a`.
//
// Like before, uses of `y` or `b_r` will keep `a` borrowed.
//
// But now it is also the case that uses of `x` or `a_r` will
// keep `'b` borrowed.
foo_1(x, y);
Or to phrase it another way, a and b have to be borrowed for the same duration. That borrow must not be active past the inner block because that's where b goes out of scope and becomes uninitialized. That's possible if you don't use x or a_r past the inner block.[4] But if you do use them, it causes the borrow check error.
So should we say foo_2 is more complicated, but allows more uses? That is true from the perspective of the caller. But from the perspective of the function body, foo_1 is more flexible, because you can make this change without breaking downstream:
This is sound because uses of x keep b borrowed with this signature. That is not the case with foo_2, and thus changing the function body results in an error. (Callers have to obey the bounds in the function signature, but so does the function body.)
So which signature is better depends on your actual use case (and these examples are all too contrived to really say).
I would say that this comment and this topic have so far been about borrow checking. That happens to involve subtyping concepts like invariance, but subtyping hasn't been the actual focus IMO. Which is fine, but I'll write a little more, in case you do want to get a better grasp on subtyping with less borrow checking specific distractions.
That's basically correct, though you may want to tighten up your terminology / syntax. I guess I would say something like...
Let Sub <: Super mean that Sub is a subtype of Super.
Given a type constructor F<X> such that X is invariant in F<X>, F<One> <: F<Two> only when One == Two exactly.
Given a type constructor F<X> such that X is covariant in F<X>, F<One> <: F<Two> only when One <: Two.
Given a type constructor F<X> such that X is contravariant in F<X>, F<One> <: F<Two> only when Two <: One.
An important detail being that every generic parameter has a variance within the context of the overall type.
From there you can go on to play around with nested generics and how variance works out for your own structs, and so on.
Here are a bunch of examples about subtypes and variance that don't involve borrow checking.
A more technical approach can be found here or in the cited paper.
