# 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 ↩︎

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, `SubType``SuperType`.

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