docs and stdlib: clean up lifetime "contravariance" story

[pnkfelix]

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.

[pnkfelix]

cc @nikomatsakis @zwarich @nick29581

[pnkfelix]

cc @aturon due to rust-lang/rust/issues/15699

[Kimundi]

Sounds like a good idea, "outliving" is a more intuitive terminology than the currently used one.

[zwarich]

This does go against the precedent for subtyping that a subtype should have fewer inhabitants than a supertype, so it's not a completely subjective choice that can just be swapped without adding confusion.

I think that the names 'contravariant' and 'covariant' are independently inadequate, and we should probably come up with replacement names for every place that we use them currently. In fact, we probably need separate names for variance in standard type kinds compared to the lifetime kind. The 'in' / 'out' names are popular for variance in other languages, but they don't make sense for lifetimes, where something like 'outlives' / ??? would be better. However, when talking about the subtyping relationship between lifetimes on the formal level, I would prefer to still use the notation that matches the standard practice.

[pnkfelix]

@zwarich what are the inhabitants of a lifetime 'a?

In particular, are the inhabitants of a lifetime 'a a collection of values (perhaps a type-indexed family of values, so that one can talk about values in 'a T) ? Or are the inhabitants of a lifetime 'a a collection of dynamic extents ? (The latter might make more sense if we adopt one of the proposals to support explicit calls of the form foo::<'a>() where 'a is a lifetime annotation on a block.)

The answer is important because I think it ends up inverting this question of "fewer inhabitants..."

---

Well, acutually, its not enough to say which kind of inhabitants we're talking about -- we also need to define up front what the relation the collection of inhabitants has with the lifetime ... for the collection of values, are they values that last only up to (but not beyond) the lifetime 'a? Or are they values that outlive 'a?

---

I guess my point is that there is no intuitive terminology here, and we might be able to choose the definitions that best solve the problems facing us.

[pnkfelix]

A good smoke test for any of these definitions is how well it handles 'static . We want 'static to be the bottom of the lifetime hierarchy (I think), in that &'static T <: &'a T for any 'a, right?

So if the inhabitants of a lifetime are the set of dynamic extents that last for that duration, then for 'static, we get the right answer: no dynamic extents survive that long. The inhabitants of 'static are then the empty set; which makes it a natural choice for the bottom of the lattice formed by <:_2

[zwarich]

@pnkfelix I am thinking in terms of the analogy of partial traces of a program's execution inhabiting lifetimes, which I guess is a bit different than a term inhabiting a type. Maybe a better word than 'inhabits' would be 'satisfies' or 'matches'?

If I have lifetimes

'a: {
    'b: { ... }
}

I would say that a partial program trace inhabits 'a if that trace is entirely contained in the portion of the program that 'a statically represents. Thus 'a has more inhabitants than 'b and it would make sense to say that 'b ≤ 'a.

With your example of 'static and this definition of inhabitation, every partial trace of program execution inhabits 'static, so 'static should be top, not bottom.

[pnkfelix]

@zwarich And why not adopt the opposite definition: that a program trace inhabits 'a if that trace entirely contains the portion of the the program that 'a statically represents?

(That is basically the same as what I meant by my hypothesized "the inhabitants of a lifetime are the set of dynamic extents that last for that duration"

I'm not claiming that this is more natural than your definition. I am rather claiming that neither definition is particularly natural.

I do think that one gets more utility out of the definition that I am writing, at least in terms of then how that set of inhabitants relates to the rest of the type system.

---

In any case, I do agree that if one adopts your definition, then you end up with 'b ≤ 'a and 'static representing the universe of traces (top), not the empty set (bottom).

But 'static being top does not seem to me like a useful way to handle 'static, considering how we deal with 'static elsewhere in the language.

[nikomatsakis]

This has been raised before. Once in the issue in question and again on discuss, where I think a comment that is more-or-less identical to this proposal was made. I think that having the name "outlives" is certainly helpful. In the past I've been pretty opposed to this but I'm slowly coming around to it. I think we should avoid the use of the prefix "sub" in general with lifetimes. So 'a : 'b is pronounced "'a outlives 'b" (that's certainly what I do in my head, same with T : 'a).

I guess my feeling is there are many intersecting questions. I'm not sure I have the dissection right here, but I think we should tease out just what is being proposed here precisely:

1. What should we do about marker traits? I should writeup my latest thoughts in an RFC. It kind of sidesteps the question to some extent by using traits to declare variance, which means that one can only "declare variance" somewhat indirectly (e.g., &'a T : Covariant). This is both a strength and a weakness of the proposal. I've been waiting till I had a complete impl but that's blocked on where clauses and it's not worth holding everything up.
2. What do write in the docs? Here I agree that &'a T <: &'b T if 'a outlives 'b is the best thing to say. It makes sense. If we later do try to explain variance, it would make sense to continue and say that Foo<'a> <: Foo<'b> if 'a outlives 'b.
3. How to formalize and think about this in the implementation? I think it probably makes sense to focus on the outlives relation as much as possible, but certainly the term "sublifetime" should always mean "a smaller lifetime". At some point you do wind up "switching direction", but I guess we can push this much deeper. It can be confusing keeping the "direction" straight, I agree. But this is also the least important part.

[pythonesque]

I'm currently using the lifetime variance and would be pretty sad to see it go away. Would the same functionality still be available?

[pnkfelix]

@pythonesque we won't be getting rid of variance in terms of linguistic expressiveness. This is largely about (1.) the terminology we use when talking about lifetimes (how they relate to each other and how they influence the subtyping relation), and (2.) how one encodes variance restrictions.

I don't think anyone is talking about making the language less expressive on this front.

[pythonesque]

Okay, thanks for clarifying!

[zwarich]

@pnkfelix Since regions are subsets of a directed graph, it makes more sense to me to use the standard subset ordering, but maybe that is because I am so brainwashed by standard mathematical notation. If you were to come up with a language that had lifetimes for some other purpose but no pointers with a lifetime, which ordering would you use?

Regardless, that discussion is irrelevant in a way, since neither 'contravariant' nor 'covariant' are great user-facing terminology. If we make a change it should probably be to something that isn't so order-theoretic.

[pnkfelix]

@zwarich I think your hypothetical "a language that had lifetimes for some other purpose but no pointers with a lifetime" shows where our views are differing: You seem to ask "what would the word 'lifetime' intutively denote", while I am trying to say that the intuitions attached to the word "lifetime" are problematic.

I think the term "lifetime", while better than "region" in the sense of Tofte/Talpin, still leads people to have the wrong intuitions about the relationships here. If I had a better term than "lifetime" at hand, I would suggest it, but unfortunately my neurons are stuck in the local web around that word ("lease", "extent").

This issue (#391) was an attempt to isolate the source of incorrect intuitions to just one spot in Rust's story, rather than having three or more floating around.

---

However, in the end that I do agree with you that "contravariant" and "covariant" are not great user-facing terminology. Nor is "sublifetime" for that matter. I agree with @nikomatsakis 's comment above: If we just shift to using the term "outlives" everywhere (for both 'b : 'a and T : 'a, and never talk about sublifetimes nor of any subtyping relationship on lifetimes), then I will probably be satisfied with that.

[zwarich]

@pnkfelix I can't come up with a better name than 'lifetime' either. We discussed the naming of contravariance / covariance in the variance discussion at the workweek.

In the workweek discussion I proposed 'longer' and 'shorter' for variance annotations of lifetime parameters, to possibly go along with 'in' and 'out' for other type parameters. We discussed whether covariance is really necessary to support, with a bit of a begrudging acceptance that we might as well support it since the underlying type theory basically has to support it anyways, and getting rid of it doesn't solve many of the problems one would hope it solves. For these reasons, we agreed to stick with markers instead of adding binding-site variance annotations in 1.0, but perhaps renaming the markers before 1.0 is a good thing to do.

[pnkfelix]

@zwarich well, as I said in the description, one of my motivations here was to say that &'a T is covariant with respect to 'a (since it is using <:_2, i.e. the outlives relation, to relate lifetimes).

An interesting consequence of that (I think) is that we would probably have much less need for the Contravariant marker. Perhaps we would not need it at all. Instead of having to come up with two or three names where two of them are opposites (corresponding to "co-" and "contra-variant" -- the third name is "invariant"), we only need the notions of "covariant" and "invariant". And if that is the case, that opens up possibilities: We could talk about "Flexible" versus "Fixed" type parameters, for example. (Just a throwaway thought before bed, maybe nonsensical.)

[nrc]

I strongly oppose using longer/shorter etc. rather than co-/contravariant. I realise covariant etc. are not well know terms, but they are google-able. longer/shorter etc. are misleading because it is only the hidden lifetime variable which is longer/shorter, the actual lifetimes must (usually) outlive the hidden lifetime, so even if it is a "shorter" variable, the actual lifetimes may in fact be longer than that bound.

That is fundamentally why co-/contravariance is confusing and trying to hide that just makes the confusion worse, not better. I think this is a rare situation where sugar coating things makes it worse for the programmer and we are better to stick to correct but scary terminology.

[zwarich]

@pnkfelix I'm not so sure that there is any problem with intuitions associated with 'lifetime', at least after putting aside the name clash issues. The idea of a lifetime as a connected portion of program execution seems pretty intuitive, and in that context 'sublifetime' would have the meaning that it currently has in Rust. This has some connection to an RFC I am about to post soon on the definition of single-entry / multiple-exit regions. That definition is strongly motivated by this concept of a lifetime.

@nick29581 I would probably prefer the correct mathematical notation for everything: lifetimes ordered by inclusion, co/contravariance having their usual meanings, etc. but I don't know how popular that is. When we add HKT we will have to come up with binding-site annotations for variance, as opposed to just having marker types. We could just accept that there is no good notation for such a thing, given the experience of the few other languages with HKT and subtyping, but maybe there's a better approach.

[nikomatsakis]

@zwarich I realized at some point that in and out carry no intutions for me in Rust, because methods are disjoint from the type definitions themselves. They make sense on traits, I guess, but is T "input" or "output" here in the definition of Option? (I think the answer is output, since out usually corresponds to Covariant, but I always expect "input" for some reason? Maybe it's just me.)

[reem]

As someone unfamiliar with co/contra-variance, I have no idea what they mean, and repeated googling has not given me anything. If we are going to stick with highly technical, esoteric names for these things, then we really have to document and explain them a lot better.

[huonw]

We do have documentation, and the wikipedia article has some examples. @reem, are there ways that can be improved that come to mind? (E.g. more Rust-specific examples?)

I'm not sure using non-technical, non-esoteric names will help much, as the concept still exists, and (as @nikomatsakis points out), most other names like in and out don't really have any correct intuition. There's the risk that alternate names will just be as jargon-y as co*variance, at worst they'll be confusing due to non-technical connotations.

(Maybe there is a set of names that work well, but I can't think of one right now. e: Oh, reading the rest of the discussion, 'longer'/'shorter', 'outlives' don't seem crazy... if they only apply to lifetimes.)

[mukilan]

Will this issue be sorted out by 1.0? I have a good understanding of co/contra-variance with respect to type parameters, but when I had to use the lifetime markers, I was extremely confused because the meanings were reversed (rust-lang/rust#15699) . I had assumed that the sub typing relations for lifetimes were based on the "outlives" relation.

If I may put my two cents in, as an average programmer, with very little knowledge of type theory and lattices, I have no problem with the terms "co/contra-variance", if it is based on the "outlives" condition (i.e the <:_2 relation proposed by @pnkfelix ) rather than in terms of "sub lifetimes". Maybe this is because in the languages I've encountered so far, variance was explained in terms of "substitutability" of types and the <:_2 relation agrees with this intuition.

[Centril]

Triage, @pnkfelix is there anything to do here?

[pnkfelix]

There has been some independent effort on revising the model one uses to describe and/or teach lifetimes. I think the choices there may effect what happens here

But I also don’t think this RFC issue is really buying us anything at this point