Struggling with the subtyping relation of lifetimes in Rust
Asked Answered
T

1

32

I feel dumb for having browsed the marker section of the Rust documentation and the Wikipedia articles about subtyping and variance multiple times without it improving my understanding of the lifetimes subtyping relation.

I think I'm just used to the "typical OOP-style" subtying relations like "Cat <: Animal" meaning "Cat is a subtype of Animal" where "S is a subtype of T" means "any term S can be safely used in a context where a term of type T is expected". So far so good.

But how does this apply to lifetimes? The way it is defined right now in Rust is apparently(*)

(#1) 'a <: 'b <=> lifetime a is no longer than lifetime b.

And you might think "Of course that's what it means!" possibly because <: looks similar to the less than operator or possibly because "sub" makes you think of subsets and a shorter lifespan is certainly a subset of a longer lifespan. But is 'a really a subtype of 'b if 'a is no longer than 'b? Let's try to apply Wikipedia's definition of the subtype relation:

(#2) 'a <: 'b <=> lifetime a can be safely used in a context where lifetime b is expected.

The problem I have is that I'm not able to reconcile this. How do you get from #2 to #1? Because to me, this seems like a contradiction... If you expect something to be alive for at least b and you have something with a lifetime a that's shorter than b, you obviously cannot use it in that context where something with a lifetime b is required, can you? Is it just me or did we get the subtyping relation for lifetimes wrong?

Edit: (*) According to Ms2ger in the #rust IRC channel this is the case. It also fits with the documentation on the contravariant lifetime marker which is used in the Items iterator.

Edit2: The ContravariantLifetime and CovariantLifetime markers have been removed. We now have PhantomData as a replacement in the marker module.

Tungting answered 20/8, 2014 at 14:40 Comment(7)
Rust's notion of lifetimes was inspired by another programming language called Cyclone and its similar concept of regions. Section 2.3 of Region-Based Memory Management in Cyclone discusses region subtyping and may prove helpful! I believe a <: b <=> lifetime b is no longer than lifetime a.Lipcombe
I think this discussion may be useful.Milly
@VladimirMatveev: It is!Tungting
I guess we just have to accept 'a <: 'b meaning "lifetime a is not longer than lifetime b" as something which was decided more or less arbitrarily, has little to do with subtyping despite the notation and is only if importance if you want to understand what the lifetime variance markers mean.Tungting
@mwhittaker: If you remember right, that would be the reverse of how "subtyping" is defined for lifetimes in Rust.Tungting
@sellibitze, I think you're right! The definition of subtypes in Rust and Cyclone seem to be opposites. Here's an excerpt from the paper I linked earlier that makes Cyclone's subtype rule rather explicit: "we observe that if the region corresponding to p1 outlives the region corresponding to p2, then it is sound to use a value of type *p1 where we expect one of type *p2"Lipcombe
The resolution to the linked GitHub issue is, "Lifetimes are not types and therefore have no subtype order; they do, however, have an ordering given by region inclusion."Kuvasz
F
10

Disclaimer: I am not exactly a CS guru, so this answer will focus on practical concepts and I will not even attempt to link it to theoretical concepts lest I make a mess of things.

I think that the issue is trying to apply the subtyping concept to something which is not a type.

  • 'a is a lifetime
  • &'a T is a type

You can compare &'a T and &'b U and see whether they obey a subtyping relationship, but you cannot establish a subtyping relationship with two lifetimes in the abstract because:

  • sometimes, in order to be substituable, the new lifetime must be greater than the replaced lifetime.
  • sometimes, in order to be substituable, the new lifetime must be smaller than the replaced lifetime.

We can check this through two simple examples.


The first example is maybe the easiest: a lifetime can be substituted if it is greater!

//  Using a lifetime as a bound
struct Reference<'a, T>
    where T: 'a
{
    data: &'a T
}

fn switch<'a, 'b, T>(r: &mut Reference<'a, T>, new: &'b T)
    where 'b: 'a
{
    r.data = new;
}

Here, the compiler only allows the substitution if 'b is at least as great as 'a which is expressed by the lifetime bound 'b: 'a. This is because Rust abhors dangling references, and thus a container may only contain references to objects that will outlive it.

When used as a guarantee, a greater lifetime is a subtype of a lesser lifetime and can be substituted in its stead. This hints as mentioned by @aturon, that in this usage 'static is a subtype of all lifetimes.


The second example is a tad trickier: a lifetime can be substituted if it is lesser!

Let's start with the following:

struct Token;

fn restrict<'a, 'b, T>(original: &'a T, _: &'b Token) -> &'b T
    where 'a: 'b
{
    original
}

The following usage is correct:

fn main() {
    let i = 4;

    {
        let lesser = Token;
        let k = restrict(&i, &lesser);
        println!("{}", k);
    }
}

And our previous demonstration said that we can substitute a greater lifetime instead of a lesser one:

fn main() {
    let greater = Token;
    let j;  // prevent unification of lifetimes

    {
        let i = 4;
        j = restrict(&i, &greater);
    }
    println!("{}", j);
}

error: `i` does not live long enough
j = restrict(&i, &greater);

When used as a constraint, a lesser lifetime is a subtype of a greater lifetime and can be substituted in its stead. In this usage, 'static is a supertype of all lifetimes.


Therefore, there is no single subtyping relationship between lifetimes because they serve two radically opposite purposes!

To recapitulate:

  • when used as a guarantee: greater <: lesser
  • when used as a constraint: lesser <: greater

Note: some lifetime can plausibly act both as a guarantee AND a constraint at the same time.

Facient answered 14/2, 2016 at 17:6 Comment(2)
I guess the keywords here are covariance (if F is covariant, then a <: b implies F(a) <: F(b)) and contravariance (if F is contravariant, a <: b implies F(b) <: F(a)).Griceldagrid
@Rhymoid: Thanks! (I have a tendency never to remember which is which...)Facient

© 2022 - 2024 — McMap. All rights reserved.