How to understand why Box<&'longer T> is a subtype of Box<&'shorter T>>

So, given Cell<T> and Cell<U>, where T:U, then Cell<T>: Cell<U>?

No, as described above that is invariant. The rule of thumb/ideal is:

  • If you can't read from it, it's covariant
  • If you can't write to it, it's contravariant
  • If you can do both, it's invariant

For rust, this is about when the name is mut, that is, it's about the type.

1 Like

So, the precondition for the statement to be true is

For generic type F, if F<T> is covariant over T, then

If T is a subtype of U, then F<T> is a subtype of F<U>

This is the complete definition, right?

Exactly.

I didn't follow this. Could you elaborate on it a bit?

It's a question of composition. If I create a

struct S<'s> {
    field: fn(fn(Vec<fn(&'s str)>)),
}

or something, is 's in S<'s> covariant, contravariant, or invariant? That is, can a freely treat an S<'medium> as an S<'short> (covariant), S<'long> (contravariant), or only as a S<'medium> (invariant)?

And there are also generic situations. What about T in S<T> if I have the below? If I make a S<&'a str>, am I going to have any flexibility to change 'a?

struct S<T> {
    field: HashMap<i32, Vec<Self> -> Rc<T>>
}

Variance is the property that answers these questions,[1] and answering these questions is necessary to make lifetimes as ergonomic as possible while still being sound. It's a well-studied area beyond Rust; better to lean on that than to try and recreate the wheel.

f(P) is contravariant in P. This means that if Q: P, f(P): f(Q). Note how they changed sides here.

So consider fn(&'short str) and fn(&'static str). &'static str: &'short str, and so by the contravariance of P in fn(P), we have

  • fn(&'short str): fn(&'static str)

Which means that if I have a fn(&'short str), I can treat it as a fn(&'static str). [2]

Note how this complements the covariance you're probably use to:

  • If a function needs a &'short str, you can feed it a &'long str
  • If a function pointer can only consume &'short str, it's okay to only feed it &'long str
  • It's okay to treat a fn(&'short str) as a fn(&'long str)

Close, but not quite. A is covariant in Vec<A>. That means that if B: A, then Vec<B>: Vec<A>. Now, let's say that A = fn(&'a str). f(P) is contravariant in P. That means that if Q: P, then f(P): f(Q), as discussed. Note again how the type variables switched sides this time.

So if I have a Vec<fn(&'short str)> (covariant over fn(...)),

  • Q: fn(&'short str) implies Vec<Q>: Vec<fn(&'short str)>
  • fn(X) is contravariant in X, so
  • Y: &'short str implies fn(&'short str): Y
    • Implies Vec<fn(&'short str)>: Vec<Y>
  • &'t T is covariant in both 't and T, so
  • 'long: 'short and U: str implies &'long U: &'short str
    • Implies fn(&'short str): fn(&'long U)
    • Implies Vec<fn(&'short str)>: Vec<fn(&'long U)>
  • Non-parameterized types are reflective only (str: str), so we can stop there

So in summary, Vec<T> is covariant in T, but the lifetime in Vec<fn(&'short str)> can be lengthened, because the lifetime was covariant contravariant [3] in T.

These recursive, compositional relationships is what variance is all about. If you were allowed to shorten the lifetime in Vec<fn(&'short str)>, that would be unsound. [4]

This is basically a rehash of what @steffahn posted earlier.

But again, it's also rare to run into complicated types in practice. It's usually only a layer or two deep.

Make a test case.


  1. or if you prefer, allows the compiler to mechanically and soundly allow flexibility where possible ↩︎

  2. In subtyping terms, fn(&'short str) is a fn(&'static str). ↩︎

  3. yes, it is hard to keep it all straight :sweat_smile: ↩︎

  4. Example: Say I have a Vec<fn(&'static str)>, and one of those function pointers launches a new thread that prints out the str every minute. If you could shorten the lifetime, you could call that function with a local String reference and then exit. The other thread will then start trying to read and print deallocated memory. ↩︎

6 Likes

Thanks. Your answers and @vague's answers are what I am looking for. You help me clear the other part: how the relationship would be if a covariant integrates with a contravariant.

I think I have got a comprehension of the key points. First, given a generic type F(precisely, a type constructor, such as an fn that can be composed with other types to form a function pointer type). If we say F is covariant in/over T, then the composed type will have the following relationship:

F<T>: F<U>, if T : U

If we say F is contravariant in/over T, then the result will be opposite to the above, that is

F<U> : F<T>, if T : U

if we say F is invariant in/over T, then whenever the context requires F<T>, we only feed it with an exact F<T>, that is

F<T>: F<U>, if and only if T=U

For a compound types, such as F0<F1<F2< ... Fn <T> ... >>> vs F0<F1<F2< ... Fn <U> ... >>>, we should compare each Fi<Ti> and Fi<Ui> to determine which is a subtype of the other, which calculates the ResultXi, then determine the relationship for Fi-1<ResultTi> and Fi-1<ResultUi>, repeat the process until F0, then we finally determine the relationship between F0<ResultT1> and F0<ResultU1>, as you have said above. Right?

1 Like

Yes, I think you have the idea now. And if a parameter shows up in more than one position, you take the GLB. Perhaps most commonly, fn(T) -> T is invariant in T, because the GLB of contravariant (argument position) and covariant (return position) is invariant.

2 Likes

Sure. It's a bit tricky to get simple examples of due to Rust not really having concrete type subtyping, but here's a general pseudocode example:

trait Pick<T> {
  fn pick() -> T;
}

trait Eat<T> {
  fn eat(item: T);
}

trait Both<T> {
  fn pick() -> T;
  fn eat(item: T);
}

// imagine we somehow have Apple and Fruit types where Apple is a subtype of Fruit

// Alice has an apple orchid
struct Alice;
impl Pick<Apple> for Alice { ... }

// Bob is hungry
struct Bob;
impl Eat<Fruit> for Bob { ... }

// Carol loves apples
struct Carol;
impl Both<Apple> for Carol { ... }

// Dave loves all fruit
struct Dave;
impl Both<Fruit> for Dave { ... }

// If you can pick Apples, you can pick Fruit.
let alice: &dyn Pick<Fruit> = &Alice;
// If you can eat Fruit, you can eat Apples.
let bob: &dyn Eat<Apple> = &Bob;
// Doesn't work: Carol can pick any fruit, but can't eat any Fruit
// let carol: &dyn Both<Fruit> = &Carol;
// Doesn't work: Dave can't pick only Apples, even if he can eat Apples
// let dave: &dyn Both<Apple> = &Dave;
1 Like

I think I have had a preliminary understanding of these concepts. For the concrete case, it may be more complex than I see it. In practice(especially, for users), is it necessary to have a sufficient understanding of these concepts? Or is it just a technique that the implementor of rust compilers should grasp?

A vague, intuitive understanding will be sufficient for most programmers, especially if they're writing safe code— If your intuition is wrong, the worst that happens is a compile error. Actually doing a variance analysis is usually reserved for figuring out why your intuition was wrong when one of those errors happens. That's not generally required for clearing the compiler error, but is useful for preemptively avoiding similar errors in future.

6 Likes

Please note that T: U is not Rust syntax for a subtype relationship: it is just a common convention.

There are four ways in which Rust uses a single : that can sometimes resemble subtyping, but aren't:

  • Type: Trait means that Type implements Trait. Traits are not types so there is no subtyping relationship. (this also does not mean that Type is a subtype of dyn Trait when Trait is object safe. Coercibility is not the same as subtyping.)
  • Type: 'lifetime means that Type is valid for at least as long as 'lifetime. Again, lifetimes aren't types, so this isn't a subtyping relationship.
  • 'lifetime: 'lifetime means that one lifetime is valid for at least as long as the other. This actually kind of is a subtype relationship, except that it's between lifetimes and not types.
  • Supertrait bounds in a trait definition, which are restrictions on what kind of types can implement the trait.

I think it's probably better to use synthetic syntax like ⊆ to indicate subtyping in the context of Rust, even though : is more common in type theory, to make it clear we're not talking about any of the above things but a relationship between types that can't be expressed in the language itself.

5 Likes

I think using is a bit confusing here. In rust, we say a longer lifetime 'longer is a subtype of the short lifetime 'shorter because the whole duration that is denoted by 'longer can be or contain 'shorter. However, in mathematics, the symbol means the left-hand stuff is contained by the right hand.

In mathematics, set A is a subset of a set B if all elements of A are also elements of B; B is then a superset of A. It is possible for A and B to be equal; if they are unequal, then A is a proper subset of B. The relationship of one set being a subset of another is called inclusion (or sometimes containment). A is a subset of B may also be expressed as B includes (or contains) A or A is included (or contained) in B.

Based on this definition, 'longer'shorter means 'longer is included in 'shorter, obviously, it is not true.

If we would prefer to use the symbol , we may say 'shorter'longer, which makes more sense. each region in 'shorter is included by 'longer but not the way around.

2 Likes

It's not that either convention makes more sense; shorter ≤ longer emphasizes the size of the region, while longer ≤ shorter describes the subtyping relationship. It all boils down to which one one is formulating in terms of the other one; neither seems more fundamental.

3 Likes

It makes more sense if you think of types as sets of values: If A is a subtype of B, then every value of type A can also be considered a value of type B, but not the other way around— This is a subset relationship, usually denoted AB.

In the case of lifetimes, every region that satisfies a ’long bound also satisfies a ’short one, so you get the somewhat unintuitive result that ’long’short. What this really means is that ’long is a stricter requirement than ’short, which in turn means that ’long represents fewer possible values than ’short does.

Aside: There’s no doubt that this terminology can be hard to reason about: If you look at the edit history of my post introducing ⊆ to this thread, you’ll see that I originally mixed up ‘subtype’ and ‘supertype’.

3 Likes

The symbol just introduces the ambiguous meaning. In mathematics, it means the right-hand set comprises the left-hand set, considering a language that has an inheritance relationship

struct SuperType{
    int a;
};
struct SubType: SuperType{
   float b;
};

In the SubType, the set has two members {a, b} while the SuperType only has one {b}. {b}{a,b} according to the definition of the symbol .

In your definition, you seem to define the symbol with the meaning that the left hand is a subtype of the right hand.

Still think the symbol in this context is contradictory to the mathematics meaning

'longer: {
    
   'shorter:{ 
      
   }
}

'longer has a larger area than that of 'shorter, hence 'shorter is a subset of 'longer.

1 Like

I do, but I’m not talking about members; I’m talking about values. If you enumerate all the possible SubType values, you'll get the set:

  • SubType { a=0, b=0.0 }
  • SubType { a=0, b=NaN }
  • SubType { a=0, b=Inf }
  • SubType { a=0, b=-Inf }
  • SubType { a=0, b=... }
  • SubType { a=1, b=0.0 }
  • SubType { a=1, b=NaN }
  • SubType { a=1, b=Inf }
  • SubType { a=1, b=-Inf }
  • SubType { a=1, b=... }
  • etc...

Per the Liskov substitutability principle, all of these must also be included in the set of valid SuperType values, which additionally includes these:

  • SuperType { a=0 }
  • SuperType { a=1 }
  • SuperType { a=2 }
  • etc...

Clearly, then, SubTypeSuperType.


The inversion comes from the fact that, in Rust, the only supported lifetime bounds are lower bounds, so the syntax 'a really represents the range of regions [a, ∞). And this is clearly true:

[long, ∞) ⊆ [short, ∞)

3 Likes

I would like to share about my intuition for SubTrait: SuperTrait.

Let's think this way:
the definition of
subset A = { types required to live for 'long lifetime } and
superset B = { types required to live for 'short lifetime }
is correct because that's to say
any type living for 'long is a type living for 'short[1].
A variable living for 'long can naturally shorten -- you can ask a variable living for 'long to just live for 'short.[2]

We don't think the case that any type living for 'short is a type living for 'long is correct:
obviously you cannot ask a variable only living for 'short to live for 'long.

The point here is to always stand in the perspective of types. Not in the perspective of lifetime itself -- the region where a value/reference is alive.


And the key concept for subtyping I learnt from Jonhoo's video, which has been posted above, is "usability".
Subtypes are more usable than supertypes for various reasons. Like for 'static: 'any, we don't manually and explicitly cast a 'static variable to a new one with a shorter lifetime, so 'static is more usable (and easy to use).


  1. equivalent to the definition in the link I share: all elements of A are also elements of B ↩︎

  2. Well, I might misuse the term variable and type. But a variable must have its specific type. ↩︎

1 Like

This is not the only kind of subtyping in Rust. We also have HRTB subtyping where for example for<'a> fn(&'a T) is a subtype of fn(&'some_concrete_lifetime T) and dyn for<'a> Trait<'a> is a subtype of dyn Trait<'some_concrete_lifetime>. While this still involves lifetimes, it doesn't work like you described.

5 Likes

Instead of thinking about it in terms of subtypes, think about it in terms of bounds. 'longer: 'shorter means 'longer requires 'shorter, same as how trait Foo: Bar {} means Foo requires Bar and how T: Add means T requires Add.

1 Like