nomicon
nomicon copied to clipboard
rust-lang
True? "In Rust, subtyping derives entirely from lifetimes." [Subtyping page]
Although it is true that Rust does not support structural subtyping nor record subtyping, it does support nominal subtyping with regard to the relationship between structs (or traits) and the trait they implement, much like the relationship in C++ between some class and the C++ abstract base it inherits from. This check is not a lifetime check, because we are not checking on lifetime scopes, but rather whether the requested type coercion is valid based on information known about the subtype relationship between the two types.
Some evidence for this is visible in the fact that Rust will flag as a compile error whenever an attempt is make to coerce a struct reference (&S) into a trait reference (&T) that the struct does not implement. Reversing them (trait to struct) will also fail. I suspect, though I have not tested it, that this subtyping check is handled properly when dealing with contravariance (e.g., fn(T) -> U). If not, shouldn't it be for the sake of type safety?
There is yet another form of subtyping that Rust supports, besides lifetime-based and trait/struct-based: the ability to coerce a reference from &mut T to &T (but not the reverse)
I would recommend broadening this sentence to say something more like: "In Rust, subtype checks focus on lifetimes, traits, and the mutability of the reference" and then provide a few extra paragraphs that briefly describe these relationships. I think it is appropriate to focus mainly on lifetimes throughout the rest of the page, as that is the most common subtyping failure that readers will run into.
These conversions are called coercions, not subtyping. They behave more like C's integer promotion. Coercions are different from subtyping in several senses: Coercions sometimes involve computation. Coercion rules are not lifted over data structures. Coercions are resolved in an ad-hoc way during type checking. Supposedly, Rust intentionally uses the different words for them to avoid confusion.
I agree with qnighy's assessment. I would probably accept a PR that highlights this difference though. For instance, this doesn't compile, because coercions aren't subtyping:
fn foo(x: &Vec<&u32>) { }
fn main() {
let y = 0;
let x: &Vec<&mut u32> = &vec![&mut y];
foo(x);
}
Yes, it is definitely a runtime coercion, converting a pure pointer to a fat pointer. So, that is true. But I believe the fact that coercion is involved does not disqualify it from also being a subtype. Coercion is an implementation detail that relates to how a value is represented in one type vs. another.
As I understand it, we use type theory/systems to do inference and to provably ensure (type) safety. The role of subtyping is to ensure that we can safely substitute a value of one type into another type (subsumption).
The basic mathematical properties that subtyping enforces are straightforward: it goes only in one direction (S->T being valid does not imply T->S), it is transitive (S->T and T->U implies S->U), and if you insist on going in both directions, it must be the same type (S->T and T->S implies S==T). As the nomicon page correctly describes, subtyping also comes with a bunch of really cool variance rules, particularly when substituting one function signature with another (the parameters are contravariant but the return value is covariant) as well as the fact that reference mutability is contravariant.
When you apply these rules to a compiler's type system, you find that it fits as helpfully to apply them to struct->trait as it is to Rust lifetimes or C++ classes. From a logical, proof-theoretic standpoint, there is no meaningful difference. Indeed, I suspect the Rust compiler does exactly that already, even to the handling of contravariance. If it did not, it would not be able to error out when S struct is not a valid subtype of a specific T trait.
To my way of thinking, the coercion that Rust performs from a struct pointer to a trait fat pointer is actually necessary in this case to ensure type safety when performing run time substitution. During the coercion, the pointer stays the same, but compositionally we add a vtable pointer to the reference so that the logic handles method dispatching correctly.
There is prior precedence for runtime coercion being valid (and necessary) as part of subtyping. For example, the wikipedia article on subtyping points out that Int64 is a subtype of Int32, since it is an always safe substitution from one type to another. Note that a runtime coercion is required to convert the 32-bit integer to a 64-bit integer.
Similarly (IIRC), C++ also performs a runtime coercion when upcasting a class pointer to a superclass pointer (which is typically seen as a subtyping relationship). Although it does not generate a fat pointer, the coerced pointer actually has a different value, pointing to some subsection of the structure it had before.
As Gankro's example further demonstrates, coercions do not necessarily mean subtyping. These two distinct concepts just happen to align as it relates to correctly subtyping/substituting a struct reference to a trait reference, and should not be confused as synonymous or even strongly related.
Addendum: Wikipedia's section on coercions as part of the subtyping article, which also seems to suggest that these two words reflect different concepts that can sometimes align, and that subtyping can exist even in the presence of coercion. As I indicate above, acknowledging it as subtyping within the context of that nomicon page plays seamlessly and helpfully with all the rules laid out for lifetimes (which don't need coercion, because they have no runtime presence).
@jondgoodwin I think you are arguing that e.g. &mut T -> &T could be a subtyping relationship. That is correct. But as a matter of fact, it is not, and @Gankro provided an example that witnesses this.
Subtyping (and coercions) is something that is defined by the language designers in a pretty arbitrary way. Of course there are soundness requirements, but there is no requirement of completeness -- just because something could be a subtype, does not mean it has to be. In Rust, the deliberate choice was made that the only subtyping is due to lifetimes (and structural rules). Your references to Wikipedia do not refute that statement. Coercions and subtyping can align, but in Rust, they do not, and for good reasons.
I think "acknowledging" coercions as subtyping would be extremely confusing, and also blatantly incorrect. The two are very different. For example:
- Subtyping is fully structural: For example, if
T <: U("Tis a subtype ofU"), thenVec<T> <: Vec<U>. Coercions do not have this property. - As a consequence of the above, subtyping preserves runtime representation: We cannot have subtyping from
Box<T>toBox<dyn Trait>, because then we'd have to be able to generate code that converts e.g.Vec<Box<T>>toVec<Box<Trait>>. We have no interest in doing that (if it even was possible in a general way, which I doubt). In contrast, coercions can change the runtime representation (code that does this transformation is inserted by the compiler).
It might be a good idea to extend the subtyping page to reference the coercions page and explain how they are different. @jondgoodwin would you be fine repurposing this issue to track that, or should I open a new issue?
Definitely file an issue against the reference, even if we want to track it here.
The reference? Oh, right, it also contains pages for both subtyping and coercions. Does it even make sense to have this in both places?
@RalfJung Thank you for your detailed response. Most importantly, yes, you may re-purpose this issue to track your suggestion. I certainly understand the importance of language designers defining terms in ways that are accurate and helpful to the language and its users. My intent here is to lower confusion for people coming from other languages, which your suggestion would help do.
If you look again, you will find I was trying to make the same point as you with regard to the relationship between coercion and subtyping. They are distinct concepts that can sometimes align. I pointed this out only because I was told by multiple sources that the examples I brought up were not subtyping examples because they were coercion examples. As you say, they can sometimes be both, but not always. So, I am not seeking any acknowledgement that coercions are always subtyping, as I do not believe that to be true.
The issue that triggered this was discussions not around &mut T to &T, but actually about the relationship between structs and trait objects, or between traits and traits. It was argued to me that Rust was vastly different in this subtyping nature vs. (say) C++ class to a property-less abstract class, Clearly there are differences, but from an ad hoc polymorphism perspective, the "subtyping" characteristics and mechanisms are remarkably similar. As with C++, types can go in only direction safely, they have runtime coercion, and variance rules apply. Similar patterns hold true for Haskell type classes. I have no dog in this hunt. Call it subtyping or not as the team feels best; I just thought it unfortunate that people come away thinking there is a vast gulf here as opposed to a rich commonality in these mechanisms. Others may not share my concern about that. I trust the team to decide what is best.
In thinking through the examples that you and @Gankro cite, I think I am understanding that the key difference seems to rest almost completely in the fact that Rust has chosen to treat Vec et all as covariant over T. Most languages make this invariant. Because Rust treats it as covariant, I can see how worlds of problems would ensue by acknowledging that a struct is a subtype of a trait it implements. In the context of the simple case, it might be accurate and helpful, but in the context where T is wrapped within various polymorphic structures it would fall apart. An explanation like this might be useful to others too, perhaps ...
I hope I have helpfully cleared up any confusion about my suggestions and intentions.
I just realized I cannot edit other people's issues in this repo, so someone else will have to do that. @Gankro? Or could you just add me to the right team? :D
@jondgoodwin TBH I do not know a sufficiently clean theoretic description of C++ to compare subtyping there with Rust. However, AFAIK classes can turn into superclasses even below pointer indirections, right? So Class** is a subtype of Superclass**. This means things are applied structurally, so I'd argue that it is most reasonable to call this subtyping, not coercions. In contrast, in Rust, &&T cannot turn into &&Trait, and in fact that wouldn't even be possible because this coercion requires some run-time effect. This does strike me as a qualitative, not just quantitative, difference.
C++ also has coercions with side-effects though, when virtual base classes are involved (where casting up/down requires offsetting the pointer). I can only assume those cannot be applied structurally. Actually, AFAIK they only happen "on request"? That would make them neither subtyping not coercions; we are talking here about mechanisms that are applied implicitly. Explicit casts are more like function calls.
But for Java (which is much easier to talk about as it is less messy than C++), it can be seen quite clearly that the "superlcass" relation is subtyping, not a coercion: For example, it is applied below arrays (T <: U implies T[] <: U[]). Java also has generics of the style ? extends Foo to emulate some form of covariance. And this has caused Java no end of pain in the form of an extremely complex type system and even some soundness bugs. Even worse, it took more than a decade (I am told) to get anything remotely resembling a theoretical model for Scala, and one of the big blockers was subtyping.
So I think it is fair to say that Rust is vastly different here, and having built a theoretical model of Rust I am very grateful for its subtyping being very weak. :)
That said, I agree those distinctions that I care about here are subtle, and probably not extremely relevant for practical use of the language most of the time.
So it seems we agree that the docs are correct, but should be improved to better teach those that care about what this subtyping vs coercions distinction really means.
@RalfJung Hmm, I misunderstood what you wrote when I wrote my comment. I think I moved the word "reference" when I read it. Tiredness. It looks like the actual suggestion here is not really in the domain of the reference. So, uh, ignore me.
@RalfJung "AFAIK classes can turn into superclasses even below pointer indirections, right?" No. I just wrote a C++ program trying to implicitly coerce Class** to Superclass**. This won't compile due to a type mismatch. Likewise, both Rust and C++ perform implicit struct/class to trait/abstract class runtime coercions under the same circumstances (including not applying them structurally), although the details of the actual coercion operation varies due to representation differences. So, I am still at a loss as to where you see a meaningful qualitative difference.
When you say "This means things are applied structurally, so I'd argue that it is most reasonable to call this subtyping, not coercions.", it sounds like you are suggesting that when subtyping exists, it must always be capable of being applied across all structures. I do not believe that subtyping requires this. Indeed that's the whole point of being able to construct types that are invariant or contravariant with regard to their parts, as we see with &mut. Also, it also still sounds like you are treating subtyping and coercions as mutually exclusive properties, when I thought we both agreed they need not be.
We agree that Java's laxity with regard to subtyping substitution is a mess. I too see it as a blessing that Rust is not following Java's footsteps here.
"So it seems we agree that the docs are correct, but should be improved to better teach those that care about what this subtyping vs coercions distinction really means." In a meaningful way, I agree because I accept that subtyping as applied to a systems programming language means something different to you (and the Rust team) than to me, and the Rust documentation should follow your meaning rather than mine. Here's how I currently understand our differences:
My view is a pragmatic, duck typing interpretation. If substitution is safe, unidirectional and follows the variance rules symptomatic of a subtyping relationship, then it is subtyping, even if substitution cannot be universally applied under all structural/representational circumstances. This is true for me regardless of whether runtime coercion is needed to help ensure safety. The downside of my interpretation is that my language documentation has to be clear in describing the circumstances in which subtyping substitution is not supported, even when it might feel as if it ought to be safe in theory.
Your view appears to be a stricter one, where if substitution cannot be performed under all structural conditions and without runtime coercion, it is not subtyping. By this interpretation, C++ does not support subtyping at all (at least with regard to ad hoc polymorphism). The downside of your interpretation is then having to explain why certain coercions (but not others) mimic subtyping type checks in the type system (i.e., are unidirectional and potentially (?) conform to some type constructor variance rules such as being invariant with &mut and contravariant in anonymous function parameters).
Both interpretations support the same sound mechanisms in Rust (and comparable mechanisms in C++). To my mind, systems programming languages struggle here because their goals are more demanding than those of other languages. Specifically, because they want to support ad hoc polymorphism AND they want to stay close to the metal in the representation of types and values (including, importantly, the explicit type representation of pointers). The benefit of these aggressive goals is safety, performance and data economy. The cost we bear is the need for runtime coercion and constraints on when runtime substitution is possible and convenient. As a result of these trade-offs, mapping pure type theory to practical system programming language semantics ends up becoming untidy somewhere.
Anyway: However the team revises the document, I am hoping that making explicit how key terms are defined and how these concepts apply to the compiler's underlying mechanics will improve people's understanding and experience with using Rust. I hope my contributions here will be valuable in accomplishing that.
It looks like the actual suggestion here is not really in the domain of the reference. So, uh, ignore me.
I am not so sure, it seems nomicon and reference overlap quite a bit here.
@jondgoodwin
it sounds like you are suggesting that when subtyping exists, it must always be capable of being applied across all structures. I do not believe that subtyping requires this. Indeed that's the whole point of being able to construct types that are invariant or contravariant with regard to their parts, as we see with &mut.
The way I see it, contravariance is a form of "applying across all structures", just the other way around. I am not too concerned with polarities here. ;)
But if every single type constructor is invariant, I find it rather meaningless to even talk of subtyping and variance. Sure, I cannot stop you from using the term, but it is a degenerate case lacking most of the usual structure. You should have at least one covariant or contravariant type constructor to start talking about subtyping. Now I am not sure if C++ has such a type constructor at all?
My view is a pragmatic, duck typing interpretation. If substitution is safe, unidirectional and follows the variance rules symptomatic of a subtyping relationship, then it is subtyping, even if substitution cannot be universally applied under all structural/representational circumstances.
I do not understand how you can even talk of variance when you also say that substitution cannot be applied under all circumstances. The very definition of (co)variance is that "whenever T <: U, then Other<T> <: Other<U>. If there is a single counterexample, you don't have covariance.
I do indeed currently not see any subtyping in C++, but you do seem to see covariance or contravariance in C++, so I am curious which types you are thinking of here. Notice that I don't think invariance "counts" here. Invariance is the absence of propagating subtyping, you shouldn't be able to point at this absence and use that to indicate the presence of anything (like subtyping).
@RalfJung Your response ascribes to me an extreme position I did not articulate nor hold. I came here with the intent to be helpful. I have acknowledged that we define the terms somewhat differently and that the Rust documentation should reflect your interpretation. Is it worth anyone's time for me to clarify what I meant, or would it be more helpful at this point for me to bow out of the discussion, and let the team sort out whether and how best to address the concerns I raised?
Sorry for putting words into your mouth, in that case I misunderstood what you were saying. I was mostly trying to understand C++ a bit better.^^
But probably most useful would be for someone to take a stab at writing some extra notes on the subtyping/coercions page about what the difference is.
My word appreciates that. Thanks. I am sorry I confused you.
I am no expert on C++, but my understanding is that the standard templates are all invariant on T. I suspect that no small part of that choice is because of the difficulty of distinguishing between a mutable vs. immutable reference. It appears, however, that C++ does support covariance and contravariance with std::function, in much the way you might expect. More than that, I should not speculate.
I am deeply grateful for your participation in this thread. Because of your explanations, I am no longer confused by why Rust describes itself the way it does. Good luck with the document changes, Rust 2018, Rustbelt, et al. I am an admirer of the work you do.
It appears, however, that C++ does support covariance and contravariance with std::function,
Ah, I see. So there is some subtyping going on it seems. Thanks for enlightening me!