rustc: co/contravariance markers for lifetimes seem backwards

[aturon]

The names for the CovariantLifetime and ContravariantLifetime markers seem backwards: they do not match the handling of lifetimes for functions, where arguments should be contravariant and results should be covariant.

Generally, a type T is a subtype of U if you can use a T anywhere a U is expected. For lifetimes, I would expect that 'a is a "subtype" of 'b if 'a is a larger scope than 'b. That would mean that 'static is a subtype of any lifetime -- so if I have a &'static T I can use it wherever &'a T is expected.

By that logic, if 'a is a larger lifetime than 'b and Foo is covariant, we should have Foo<'a> is a subtype of Foo<'b>, and the opposite if Foo is contravariant. These notions of variance line up correctly with Rust's closure types, which follow the typical rules:

• The result position is covariant, so that |T| -> &'static U is usable wherever |T| -> &'a U is expected.
• The argument position is contravariant, so that |&'a T| -> U is usable wherever |&'static T| -> U is expected.

But the CovariantLifetime and ContravariantLifetime markers seem to work backwards from everything described above. In particular, function arguments are treated as if they had the _co_variant marker, which is very surprising:

Update After discussion with @zwarich below, I think the real culprit here is that & takes its lifetime contravariantly, while it takes its type covariantly. I don't understand the rationale behind this choice. As I argue above, I think lifetime subtyping should be reverse region inclusion, which would mean & is _co_variant.

use std::kinds::marker::{CovariantLifetime, ContravariantLifetime};

// A straight-up reference:     'static => 'a
fn test_ref<'a>(t: &'static u8) -> &'a u8 {
    t
}

// Reference in a struct:       'static => 'a
struct Foo<'a> {
    t: &'a u8
}
fn test_struct<'a>(f: Foo<'static>) -> Foo<'a> {
    f
}

// fn with arg:                 'a => 'static
fn test_fn_in<'a, 'b>(f: |&'a u8|: 'b) -> |&'static u8|: 'b {
    f
}
// fn with result:              'static => 'a
fn test_fn_out<'a, 'b>(f: ||: 'b -> &'static u8) -> (||: 'b -> &'a u8) {
    f
}

// Covariant struct:            'a => 'static
struct FooCo<'a> {
    marker: CovariantLifetime<'a>
}
fn test_co<'a>(f: FooCo<'a>) -> FooCo<'static> {
    f
}

// Contravariant struct:        'static => 'a
struct FooContra<'a> {
    marker: ContravariantLifetime<'a>
}
fn test_contra<'a>(f: FooContra<'static>) -> FooContra<'a> {
    f
}

cc @nikomatsakis @pnkfelix @pcwalton

Nominating.

[zwarich]

I think this depends on the intended interpretation of lifetimes. If the intended interpretation is that a lifetime is a control-flow region, then the subtyping relation on lifetimes should probably be inclusion, e.g. 'a ≤ 'b when the control-flow region represented by 'a is included in the control-flow region represented by 'b.

Of course, lifetimes are never used without being applied to a type constructor, and the type constructor &'a T is contravariant in 'a. I think the rules are consistent when you view them this way.

[aturon]

@zwarich You're right, these rules are consistent given that the & type constructor is _contra_variant in its lifetime. So maybe the question I should be asking is: does that make sense?

Subtyping orders are set up so that if T is a subtype of U, then you can consume a T wherever a U is expected. My intuition is that a borrow that lives longer is usable any time you expect a borrow that lives shorter. That is, larger lifetimes are subtypes of smaller ones, so the subtyping order should be the reverse of the region inclusion order and & becomes contravariant.

But maybe my intuition is wrong?

In any case, there's no breakage here; as far as I can see we can either:

• Stay with what we have, where lifetime subtyping = lifetime inclusion and & is contravariant, which I found surprising, or
• Reverse what we have, so lifetime subtyping = reverse lifetime inclusion and & is covariant. (This would require swapping the few uses of the marker types as well.)

I'm wondering if there's a good intuition or argument for the current ordering.

[zwarich]

@aturon If the & type constructor is contravariant, then the bottom value of the (lifetime) type lattice is the empty region and the top value is 'static. If the & type constructor is covariant, then the bottom value of the type lattice is 'static and the top value is the empty region. I feel like the former interpretation makes more sense given the standard bias against inhabitation of bottom.

[aturon]

@zwarich I agree with the correspondence about the ordering, but I'm wondering if there's an argument for why the former setup makes more sense?

In particular, & is a two-argument type constructor, and it's contravariant in the lifetime but covariant in the type:

// the type &'static u8 is a subtype of &'a u8:
fn basic_subtyping<'a>(f: &'static u8) -> &'a u8 {
    f
}

// the & type constructor is covariant in the type position:
fn covariant_in_type_position<'a>(f: &'static (&'static u8)) -> &'static (&'a u8) {
    f
}

Why?

[zwarich]

@aturon I don't see why I would intuitively expect a type constructor with parameters from distinct kinds to have the same variance in both. I can create type constructors with similar behavior in Rust with two parameters of the same kind, e.g.

struct A<S, T> {
    x: S,
    y: |T|:'static,
}

I think the best argument is that lifetime subtyping should be definitely be inclusion when viewed in isolation on its own merits, and everything else follows logically from that.

[aturon]

@zwarich Sorry I wasn't clear: I'm not saying that I expect every multiparameter type constructor to have the same variance in all its arguments. I'm just trying to understand the rationale for discrepant variances for &.

It seems like we agree that the choice of subtyping order on lifetimes is "arbitrary" in the sense that we can flip it if we also flip & to be covariant?

So given that we can make the choice, I'm trying to understand why we would go one way or the other.

I think the best argument is that lifetime subtyping should be definitely be inclusion when viewed in isolation on its own merits.

I don't really understand this argument: it just seems like an assertion that the current setup is the right one? I understand that we have different intuitions, but I'm trying to figure out where/whether those intuitions are grounded.

The argument I've given a couple of times above is that subtyping, formally, is set up so that if T is a subtype of U then T is usable when U is expected. As I've also mentioned, for lifetimes/borrowing a larger region is usable when a smaller region is requested, which suggests subtyping should be reverse region inclusion.

Do you disagree with that characterization? How do you see it?

[zwarich]

@aturon I don't think that the choice of ordering of lifetimes is arbitrary, since there is a convention in type theory to limit the inhabitation of bottom. If we flip the ordering then every lifetime inhabits bottom, as opposed to the current situation where no lifetime inhabits bottom. It also disagrees with well established mathematical convention for subset lattices.

Another way to think about it is like this: if you view an element of the type lattice as providing information about a term, then either the subtype ordering T ≤ U should correspond to either T providing more specific information than U or less specific information.

The generally accepted interpretation in mathematical logic and type theory (although not completely universal, e.g. some program analysis papers do the reverse) is that it means that T provides more specific information. This matches what we do today with lifetimes, that if 'a is a more specific region than 'b then 'a ≤ 'b (and vice-versa). This also matches what we do today for borrowed pointer types, if &'a T ≤ &'b U then &'a T provides more specific information about a term than &'b U. This choice is admittedly arbitrary, but to be consistent between lifetimes and types of ordinary kinds we would have to flip the ordering in both cases, so then &'a T would be covariant in 'a and contravariant in T.

[nrc]

I had a bit of a think about this. My initial intuition was with @aturon that the lifetime which admits the most uses should be the 'subtype'. I don't buy the uninhabited bottom argument because I think the real bottom is the infinite lifetime (or, perhaps the infinite set of infinite lifetimes), and 'static is just the lowest lifetime in the lattice which we care about from the perspective of Rust programs.

But, on second thoughts, lifetimes are not types and sub-lifetimes are not subtypes. I believe we are implicitly considering &'a T and not just 'a. Sub-lifetimes should just be a partial order over lifetimes and the 'smaller' lifetime should be the sub-lifetime and the 'larger' should be the super-, as if we were talking about < for integers. In this view, it makes sense for the longest lifetime (`'static') to be top.

I believe we are misled by thinking of subtyping here - subtyping is the way around that it is because its semantics are based on subsets - the smaller set of objects is on the left, the larger is on the right. That the subtype is accepted in more places than the supertype is a consequence of the set-interpretation, it is not intrinsic to the relation.

[pnkfelix]

I think much of the confusion here stems from intuitions that we attach to words like "region" and "lifetime", even though those intuitions may work against us.

For example, I like zwarich (and the code base) thought that obviously 'a <= 'b should be synonymous with "the dynamic extent represented by 'a is covered by that of 'b".

But perhaps that originates from our intuition about the word "lifetime" and one person being born and dying during the course of another's life.

If we used different terms, perhaps the intuition would flip, or at least would not be present. E.g. "tombstone", well the particular word is not my point. My point is: Is our current terminology working for or against us?

---

Anyway, even if we stick with the term "lifetime", I aim inclined to just say that there is a "stronger-than" relation on lifetimes, written 'a <: 'b, and 'a <: 'b is defined to be 'a >= 'b, and then define everything else in terms of (<:), Because I think that will serve better when it comes to reasoning about substitutability and behavioral subtyping.

[pnkfelix]

(In other words: I want to agree with @aturon, but it will not be generally palatable without some other shifts in mindset. )