docs and stdlib: clean up lifetime "contravariance" story · Issue #391 · rust-lang/rfcs (original) (raw)

Executive Summary: Switch everywhere to saying that the subtyping relationship on lifetimes is the "outlives" relationship, not the "contained within" relationship (which is the opposite). This allows for a more consistent story overall in terms of substitutability, covariance, and our bounds syntax.

We currently say in many places that the reference type constructor & (as in &'a T) is contravariant with respect to the lifetime parameter 'a. The term bleeds into the compiler internals and also even the standard library with its ContravariantLifetime marker.

The reason for this is that historically, we used to (and maybe still currently) say, "intuitively," that if the lifetime 'a is entirely contained within the lifetime 'b, then 'a is a "sub-lifetime" of 'b, and therefore if we want some sort of ordering relation <:_1 on lifetimes, it seems like 'a <:_1 'b should denote "'a is entirely contained within 'b". This is also referred to as "region inclusion" in some contexts.

(I'm putting the subscript "_1" in order to ensure that the subsequent text is entirely unambiguous.)

Once you establish that, and if you also want to determine how &'a T and &'b T are related in terms of behavioral subtyping (i.e. substitutability), then one reasons (correctly) that one reference to T is only soundly substitutable for another reference to T if the data of the first reference lives at least as long as that of the second. I.e. the relation &'x T <: &'y T should only hold if the lifetime 'x lives at least as long as 'y -- in other words, "the lifetime 'y is entirely contained within the lifetime 'x". Note that the latter is denoted by "'y <:_1 'x.

This means that if you use this first definition for a subtyping relation on lifetimes, then &'a T is indeed contravariant with respect to 'a: &'a T <: &'b T only if 'b <:_1 'a. That's how we got where we are today, where we keep talking about lifetimes being contravariant.

Meanwhile, despite the above reasoning, we went ahead and added a lifetime-bounds syntax for formal lifetime parameters, like so:

type B = Box<int>;
fn foo<'a, 'b:'a>(p: &Foo<'b>, callback: |&'a B| -> B) { ... }

struct Foo<'x> { ... }
impl<'x> Foo<'x> { fn ptr(&self) -> &'x B { ... } }

The syntax 'b:'a means "'b outlives 'a": so in the above, p.ptr(): &'b B, and &'b B <: &'a B, and therefore a call callback(p.ptr()) will be legal in the body of foo.

(There was a good motivation for using the syntax 'b:'a to mean "'b outlives 'a", rather than the alternative like fn foo<'b, 'a:'b> to mean "'a is contained within 'b", but I am having difficulty writing a succinct summary of that motivation here. Assuming an RFC gets drafted for the proposal I am writing here, it would be good for that RFC to contain such a motivation.)

Note that the above means that the bound syntax 'b: 'a corresponds to implying the relation 'a <:_1 'b : that was not a mistake, the order got deliberately switched!

So, we ourselves have been using the intuitive 'a <:_1 'b relationship and then suffering with the consequences. I suggest that we draft an RFC proposing the opposite. We throw away every trace of the a <:_1 'b relation. We define 'b <:_2 'a as the subtyping relationship on lifetimes, where one pronounces it as "'b outlives 'a". I suspect there is also some way to motivate this in terms of substitutability, something like "if 'b outlives 'a and T is a subtype of S, then a value of type T with lifetime 'b can be substituted for a value of type S with lifetime 'a." (Or more formally, a value of type T with lifetime 'b can be used in an expression context that is expecting a value of type S with lifetime 'a.)

We then can say that the type constructor & as in &'a T is covariant with respect to both 'a and T; no more having to explain what contravariance is supposed to mean. And our bounds syntax fn foo<'a, 'b:'a>(...) will actually make sense in terms of saying that 'b is beneath 'a in the subtyping relationship.