So, given Cell<T>
and Cell<U>
, where T:U
, then Cell<T>: Cell<U>
?
No, as described above that is invariant. The rule of thumb/ideal is:
- If you can't read from it, it's covariant
- If you can't write to it, it's contravariant
- If you can do both, it's invariant
For rust, this is about when the name is mut, that is, it's about the type.
So, the precondition for the statement to be true is
For generic type
F
, ifF<T>
is covariant overT
, thenIf
T
is a subtype ofU
, thenF<T>
is a subtype ofF<U>
This is the complete definition, right?
Exactly.
I didn't follow this. Could you elaborate on it a bit?
It's a question of composition. If I create a
struct S<'s> {
field: fn(fn(Vec<fn(&'s str)>)),
}
or something, is 's
in S<'s>
covariant, contravariant, or invariant? That is, can a freely treat an S<'medium>
as an S<'short>
(covariant), S<'long>
(contravariant), or only as a S<'medium>
(invariant)?
And there are also generic situations. What about T
in S<T>
if I have the below? If I make a S<&'a str>
, am I going to have any flexibility to change 'a
?
struct S<T> {
field: HashMap<i32, Vec<Self> -> Rc<T>>
}
Variance is the property that answers these questions,[1] and answering these questions is necessary to make lifetimes as ergonomic as possible while still being sound. It's a well-studied area beyond Rust; better to lean on that than to try and recreate the wheel.
f(P)
is contravariant in P
. This means that if Q: P
, f(P): f(Q)
. Note how they changed sides here.
So consider fn(&'short str)
and fn(&'static str)
. &'static str: &'short str
, and so by the contravariance of P
in fn(P)
, we have
fn(&'short str): fn(&'static str)
Which means that if I have a fn(&'short str)
, I can treat it as a fn(&'static str)
. [2]
Note how this complements the covariance you're probably use to:
- If a function needs a
&'short str
, you can feed it a&'long str
- If a function pointer can only consume
&'short str
, it's okay to only feed it&'long str
- It's okay to treat a
fn(&'short str)
as afn(&'long str)
Close, but not quite. A
is covariant in Vec<A>
. That means that if B: A
, then Vec<B>: Vec<A>
. Now, let's say that A = fn(&'a str)
. f(P)
is contravariant in P
. That means that if Q: P
, then f(P): f(Q)
, as discussed. Note again how the type variables switched sides this time.
So if I have a Vec<fn(&'short str)>
(covariant over fn(...)
),
Q: fn(&'short str)
impliesVec<Q>: Vec<fn(&'short str)>
fn(X)
is contravariant inX
, soY: &'short str
impliesfn(&'short str): Y
- Implies
Vec<fn(&'short str)>: Vec<Y>
- Implies
&'t T
is covariant in both't
andT
, so'long: 'short
andU: str
implies&'long U: &'short str
- Implies
fn(&'short str): fn(&'long U)
- Implies
Vec<fn(&'short str)>: Vec<fn(&'long U)>
- Implies
- Non-parameterized types are reflective only (
str: str
), so we can stop there
So in summary, Vec<T>
is covariant in T
, but the lifetime in Vec<fn(&'short str)>
can be lengthened, because the lifetime was covariant contravariant [3] in T
.
These recursive, compositional relationships is what variance is all about. If you were allowed to shorten the lifetime in Vec<fn(&'short str)>
, that would be unsound. [4]
This is basically a rehash of what @steffahn posted earlier.
But again, it's also rare to run into complicated types in practice. It's usually only a layer or two deep.
or if you prefer, allows the compiler to mechanically and soundly allow flexibility where possible ↩︎
In subtyping terms,
fn(&'short str)
is afn(&'static str)
. ↩︎yes, it is hard to keep it all straight ↩︎
Example: Say I have a
Vec<fn(&'static str)>
, and one of those function pointers launches a new thread that prints out thestr
every minute. If you could shorten the lifetime, you could call that function with a localString
reference and then exit. The other thread will then start trying to read and print deallocated memory. ↩︎
Thanks. Your answers and @vague's answers are what I am looking for. You help me clear the other part: how the relationship would be if a covariant integrates with a contravariant.
I think I have got a comprehension of the key points. First, given a generic type F
(precisely, a type constructor, such as an fn
that can be composed with other types to form a function pointer type). If we say F
is covariant in/over T
, then the composed type will have the following relationship:
F<T>: F<U>
, ifT : U
If we say F
is contravariant in/over T
, then the result will be opposite to the above, that is
F<U> : F<T>
, ifT : U
if we say F
is invariant in/over T
, then whenever the context requires F<T>
, we only feed it with an exact F<T>
, that is
F<T>: F<U>
, if and only ifT=U
For a compound types, such as F0<F1<F2< ... Fn <T>
... >>> vs F0<F1<F2< ... Fn <U>
... >>>, we should compare each Fi<Ti> and Fi<Ui> to determine which is a subtype of the other, which calculates the ResultXi, then determine the relationship for Fi-1<ResultTi> and Fi-1<ResultUi>, repeat the process until F0, then we finally determine the relationship between F0<ResultT1> and F0<ResultU1>, as you have said above. Right?
Yes, I think you have the idea now. And if a parameter shows up in more than one position, you take the GLB. Perhaps most commonly, fn(T) -> T
is invariant in T
, because the GLB of contravariant (argument position) and covariant (return position) is invariant.
Sure. It's a bit tricky to get simple examples of due to Rust not really having concrete type subtyping, but here's a general pseudocode example:
trait Pick<T> {
fn pick() -> T;
}
trait Eat<T> {
fn eat(item: T);
}
trait Both<T> {
fn pick() -> T;
fn eat(item: T);
}
// imagine we somehow have Apple and Fruit types where Apple is a subtype of Fruit
// Alice has an apple orchid
struct Alice;
impl Pick<Apple> for Alice { ... }
// Bob is hungry
struct Bob;
impl Eat<Fruit> for Bob { ... }
// Carol loves apples
struct Carol;
impl Both<Apple> for Carol { ... }
// Dave loves all fruit
struct Dave;
impl Both<Fruit> for Dave { ... }
// If you can pick Apples, you can pick Fruit.
let alice: &dyn Pick<Fruit> = &Alice;
// If you can eat Fruit, you can eat Apples.
let bob: &dyn Eat<Apple> = &Bob;
// Doesn't work: Carol can pick any fruit, but can't eat any Fruit
// let carol: &dyn Both<Fruit> = &Carol;
// Doesn't work: Dave can't pick only Apples, even if he can eat Apples
// let dave: &dyn Both<Apple> = &Dave;
I think I have had a preliminary understanding of these concepts. For the concrete case, it may be more complex than I see it. In practice(especially, for users), is it necessary to have a sufficient understanding of these concepts? Or is it just a technique that the implementor of rust compilers should grasp?
In practice(especially, for users), is it necessary to have a sufficient understanding of these concepts?
A vague, intuitive understanding will be sufficient for most programmers, especially if they're writing safe code— If your intuition is wrong, the worst that happens is a compile error. Actually doing a variance analysis is usually reserved for figuring out why your intuition was wrong when one of those errors happens. That's not generally required for clearing the compiler error, but is useful for preemptively avoiding similar errors in future.
Please note that T: U
is not Rust syntax for a subtype relationship: it is just a common convention.
There are four ways in which Rust uses a single :
that can sometimes resemble subtyping, but aren't:
-
Type: Trait
means thatType
implementsTrait
. Traits are not types so there is no subtyping relationship. (this also does not mean thatType
is a subtype ofdyn Trait
whenTrait
is object safe. Coercibility is not the same as subtyping.) -
Type: 'lifetime
means thatType
is valid for at least as long as'lifetime
. Again, lifetimes aren't types, so this isn't a subtyping relationship. -
'lifetime: 'lifetime
means that one lifetime is valid for at least as long as the other. This actually kind of is a subtype relationship, except that it's between lifetimes and not types. - Supertrait bounds in a trait definition, which are restrictions on what kind of types can implement the trait.
I think it's probably better to use synthetic syntax like ⊆ to indicate subtyping in the context of Rust, even though : is more common in type theory, to make it clear we're not talking about any of the above things but a relationship between types that can't be expressed in the language itself.
I think it's probably better to use synthetic syntax like ⊆ to indicate subtyping in the context of Rust
I think using ⊆
is a bit confusing here. In rust, we say a longer lifetime 'longer
is a subtype of the short lifetime 'shorter
because the whole duration that is denoted by 'longer
can be or contain 'shorter
. However, in mathematics, the symbol ⊆
means the left-hand stuff is contained by the right hand.
In mathematics, set A is a subset of a set B if all elements of A are also elements of B; B is then a superset of A. It is possible for A and B to be equal; if they are unequal, then A is a proper subset of B. The relationship of one set being a subset of another is called inclusion (or sometimes containment). A is a subset of B may also be expressed as B includes (or contains) A or A is included (or contained) in B.
Based on this definition, 'longer
⊆ 'shorter
means 'longer
is included in 'shorter
, obviously, it is not true.
If we would prefer to use the symbol ⊆
, we may say 'shorter
⊆ 'longer
, which makes more sense. each region in 'shorter
is included by 'longer
but not the way around.
It's not that either convention makes more sense; shorter ≤ longer
emphasizes the size of the region, while longer ≤ shorter
describes the subtyping relationship. It all boils down to which one one is formulating in terms of the other one; neither seems more fundamental.
Based on this definition,
'longer
⊆'shorter
means'longer
is included in'shorter
, obviously, it is not true.If we would prefer to use the symbol
⊆
, we may say'shorter
⊆'longer
, which makes more sense. each region in'shorter
is included by'longer
but not the way around.
It makes more sense if you think of types as sets of values: If A is a subtype of B, then every value of type A can also be considered a value of type B, but not the other way around— This is a subset relationship, usually denoted A ⊆ B.
In the case of lifetimes, every region that satisfies a ’long
bound also satisfies a ’short
one, so you get the somewhat unintuitive result that ’long
⊆ ’short
. What this really means is that ’long
is a stricter requirement than ’short
, which in turn means that ’long
represents fewer possible values than ’short
does.
Aside: There’s no doubt that this terminology can be hard to reason about: If you look at the edit history of my post introducing ⊆ to this thread, you’ll see that I originally mixed up ‘subtype’ and ‘supertype’.
If A is a subtype of B, then every value of type A can also be considered a value of type B, but not the other way around
The symbol ⊆
just introduces the ambiguous meaning. In mathematics, it means the right-hand set comprises the left-hand set, considering a language that has an inheritance relationship
struct SuperType{
int a;
};
struct SubType: SuperType{
float b;
};
In the SubType
, the set has two members {a, b}
while the SuperType
only has one {b}
. {b}
⊆ {a,b}
according to the definition of the symbol ⊆
.
In your definition, you seem to define the symbol ⊆
with the meaning that the left hand is a subtype of the right hand.
In the case of lifetimes, every region that satisfies a
’long
bound also satisfies a’short
one, so you get the somewhat unintuitive result that’long
⊆’short
.
Still think the symbol ⊆
in this context is contradictory to the mathematics meaning
'longer: {
'shorter:{
}
}
'longer
has a larger area than that of 'shorter
, hence 'shorter
is a subset of 'longer
.
In the
SubType
, the set has two members{a, b}
while theSuperType
only has one{b}
.{b}
⊆{a,b}
according to the definition of the symbol⊆
.In your definition, you seem to define the symbol
⊆
with the meaning that the left hand is a subtype of the right hand.
I do, but I’m not talking about members; I’m talking about values. If you enumerate all the possible SubType
values, you'll get the set:
SubType { a=0, b=0.0 }
SubType { a=0, b=NaN }
SubType { a=0, b=Inf }
SubType { a=0, b=-Inf }
SubType { a=0, b=... }
SubType { a=1, b=0.0 }
SubType { a=1, b=NaN }
SubType { a=1, b=Inf }
SubType { a=1, b=-Inf }
SubType { a=1, b=... }
- etc...
Per the Liskov substitutability principle, all of these must also be included in the set of valid SuperType
values, which additionally includes these:
SuperType { a=0 }
SuperType { a=1 }
SuperType { a=2 }
- etc...
Clearly, then, SubType
⊆ SuperType
.
'longer
has a larger area than that of'shorter
, hence'shorter
is a subset of'longer
.
The inversion comes from the fact that, in Rust, the only supported lifetime bounds are lower bounds, so the syntax 'a
really represents the range of regions [a, ∞). And this is clearly true:
[long, ∞) ⊆ [short, ∞)
I would like to share about my intuition for SubTrait: SuperTrait
.
Let's think this way:
the definition of
subset A = { types required to live for 'long lifetime }
and
superset B = { types required to live for 'short lifetime }
is correct because that's to say
any type living for 'long is a type living for 'short[1].
A variable living for 'long
can naturally shorten -- you can ask a variable living for 'long to just live for 'short.[2]
We don't think the case that any type living for 'short
is a type living for 'long
is correct:
obviously you cannot ask a variable only living for 'short to live for 'long.
The point here is to always stand in the perspective of types. Not in the perspective of lifetime itself -- the region where a value/reference is alive.
And the key concept for subtyping I learnt from Jonhoo's video, which has been posted above, is "usability".
Subtypes are more usable than supertypes for various reasons. Like for 'static: 'any
, we don't manually and explicitly cast a 'static
variable to a new one with a shorter lifetime, so 'static
is more usable (and easy to use).
What is the purpose we define the relationship in terms of covariant, invariant, and contravariant in rust? My rough impression about them is we only care how the
lifetime
in the source type would be changed to that that is suitable for the destination type. My rough understanding of covariant is that, if we say somethingA
inT
is covariant, that means a longer lifetime inA
can be shrunk to be a shorter lifetime in order to match the destination type. Invariant means the lifetime cannot be changed at all whatever how the lifetime would be longer than that in the destination type. Not sure whether this is a correct understanding.
This is not the only kind of subtyping in Rust. We also have HRTB subtyping where for example for<'a> fn(&'a T)
is a subtype of fn(&'some_concrete_lifetime T)
and dyn for<'a> Trait<'a>
is a subtype of dyn Trait<'some_concrete_lifetime>
. While this still involves lifetimes, it doesn't work like you described.
In this example, I know
'longer
is a subtype of'shorter
since'longer : 'shorter
Instead of thinking about it in terms of subtypes, think about it in terms of bounds. 'longer: 'shorter
means 'longer
requires 'shorter
, same as how trait Foo: Bar {}
means Foo
requires Bar
and how T: Add
means T
requires Add
.