-
Notifications
You must be signed in to change notification settings - Fork 12.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
rustc: co/contravariance markers for lifetimes seem backwards #15699
Comments
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. Of course, lifetimes are never used without being applied to a type constructor, and the type constructor |
@zwarich You're right, these rules are consistent given that the Subtyping orders are set up so that if But maybe my intuition is wrong? In any case, there's no breakage here; as far as I can see we can either:
I'm wondering if there's a good intuition or argument for the current ordering. |
@aturon If the |
@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, // 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? |
@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. |
@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 So given that we can make the choice, I'm trying to understand why we would go one way or the other.
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 Do you disagree with that characterization? How do you see it? |
@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 |
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 But, on second thoughts, lifetimes are not types and sub-lifetimes are not subtypes. I believe we are implicitly considering 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. |
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. |
(In other words: I want to agree with @aturon, but it will not be generally palatable without some other shifts in mindset. ) |
Thanks for the replies, everyone! I think @nick29581 is right: the subtyping relationship is on So I'm happy to close this ticket with the following new intuition:
|
The names for the
CovariantLifetime
andContravariantLifetime
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 ofU
if you can use aT
anywhere aU
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
andFoo
is covariant, we should haveFoo<'a>
is a subtype ofFoo<'b>
, and the opposite ifFoo
is contravariant. These notions of variance line up correctly with Rust's closure types, which follow the typical rules:|T| -> &'static U
is usable wherever|T| -> &'a U
is expected.|&'a T| -> U
is usable wherever|&'static T| -> U
is expected.But the
CovariantLifetime
andContravariantLifetime
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.cc @nikomatsakis @pnkfelix @pcwalton
Nominating.
The text was updated successfully, but these errors were encountered: