Rewrite the chapter on subtyping and variance #340

conradludgate · 2022-02-10T13:57:45Z

This is to address the issues raised in #339

src/subtyping.md

T-Dark0 · 2022-02-10T21:13:20Z

src/subtyping.md


 * `Vec<T>` and all other owning pointers and collections follow the same logic as `Box<T>`
 * `Cell<T>` and all other interior mutability types follow the same logic as `UnsafeCell<T>`
+* `UnsafeCell<T>` having interior mutability gives it the same variance properties as `&mut T`


It might be worth explaining that technically UnsafeCell on its own could be covariant, but that would be unsound when you form &UnsafeCell<T>, just to avoid confusing people that realize that an owned UnsafeCell<T> is equivalent to T

Can you think of a good way to explain that?

The original mostly just says that since UnsafeCell<T> allows you to treat a &T as a &mut T, it should have the same invariance

src/subtyping.md

Noratrieb

I really liked the rewrite, it's shorter and clearer, explaining everything without cats and dogs.

Small suggestion: I'd use the cool new formatting syntax

Noratrieb · 2022-02-10T21:28:23Z

src/subtyping.md

-fn love(pet: Animal) {
-    pet.snuggle();
+fn debug<T: std::fmt::Debug>(a: T, b: T) {
+    println!("a = {:?} b = {:?}", a, b);


Suggested change

println!("a = {:?} b = {:?}", a, b);

println!("a = {a:?} b = {b:?}");

This raises the MSRV of the nomicon examples, but I think we can take that :). Same for the other examples.

mejrs

Thanks, this is much better :)

src/subtyping.md

nrc · 2022-02-24T15:18:15Z

src/subtyping.md


-By default, static types must match *exactly* for a program to compile. As such,
-this code won't compile:
+Let's define that `Sub` is a subtype of `Super` (we'll be using the notation `Sub: Super` throughout this chapter)


It might be clearer to use <: for subtyping and reserve : for the outlives relation on lifetimes

Aren't these two the same thing? 'a outlives 'b means that 'a is a subtype of 'b

I don't think outlives is a subtype relation because lifetimes are not types, it could be called sub-lifetimes, but we don't call it that.

Aren't these two the same thing? 'a outlives 'b means that 'a is a subtype of 'b

That's actually the opposite of what's true: 'a: 'b means 'a T <: 'b T.

Since we don't have a notation for subtyping (: is the notation for bounds), I don't dislike the idea of using <: for subtyping types. But in order to be consistent, (since, for instance, when talking about &'lt T, we'll have to talk about 'a : 'b and about T <: U), it will then be important to distinguish covariance in a lifetime parameter, and covariance in type parameter.

Note also that I'm personally quite fond of using 'a ⊇ 'b for lifetimes, since it does match a bit better the intuition that people will have of lifetimes.

Example:

T<'lt> is covariant (in 'lt) iff when 'a ⊇ 'b, T<'a> <: T<'b>

F<T> is covariant (in T) iff when T <: U, F<T> <: F<U>

nrc · 2022-02-24T15:24:33Z

src/subtyping.md

-let mr_snuggles: Cat = ...;
-love(mr_snuggles);         // ERROR: expected Animal, found Cat
-```
+What this is suggesting to us is that the set of *requirements* that `Super` defines


I'm not sure if requirements is the best word here. Perhaps it is better to use terminology like "A value which has type Sub can be used in any way that a value of type Super can, and possibly more"

nrc · 2022-02-24T15:25:59Z

src/subtyping.md


-Or more concretely: anywhere an Animal is expected, a Cat or Dog will also work.
+Here, we have that `Error: fmt::Display` (`Error` is a *subtype* of `Display`),
+because it has all the requirements of `fmt::Display`, plus the `source`/`description`/`cause` functions.


Hmm, this is not quite right: subtyping is nominal Error <: Display because Display is declared as a super-trait of Error. That is sound because declaring a supertrait means that the subtrait inherits the supertrait's, methods.

src/subtyping.md

nrc · 2022-02-24T15:31:26Z

src/subtyping.md

-Variance is a property that *type constructors* have with respect to their
-arguments. A type constructor in Rust is any generic type with unbound arguments.
+Variance is the way that Rust defines the relationships of subtypes through their *type constructor*.
+A type constructor is any generic type with unbound arguments.


This statement might be confusing because of the multiple meanings of bound here, readers are likely to think of trait bounds rather than bound/free variables. Also, strictly speaking, type constructors are not types in Rust since we don't have HKTs.

src/subtyping.md

jyn514

I like the idea of using lifetimes to start instead of the cat + dog examples :) I only skimmed the PR, but it would be nice to have an example of why fn borrow<'a>(x: &'a Chunk<'a>) {} works (usually) but fn borrow_mut<'a>(x: &'a mut Chunk<'a>) {} is almost impossible to use. https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=1eed7dc7b916058c4a06a7da908717e4

danielhenrymantilla

I would very much not mix traits into this chapter ⚠️, but other than that, I'm quite fond of this PR 🙂 ✅

danielhenrymantilla · 2022-02-25T16:51:32Z

src/subtyping.md


-By default, static types must match *exactly* for a program to compile. As such,
-this code won't compile:
+Let's define that `Sub` is a subtype of `Super` (we'll be using the notation `Sub: Super` throughout this chapter)


Since we don't have a notation for subtyping (: is the notation for bounds), I don't dislike the idea of using <: for subtyping types. But in order to be consistent, (since, for instance, when talking about &'lt T, we'll have to talk about 'a : 'b and about T <: U), it will then be important to distinguish covariance in a lifetime parameter, and covariance in type parameter.

Note also that I'm personally quite fond of using 'a ⊇ 'b for lifetimes, since it does match a bit better the intuition that people will have of lifetimes.

Example:

T<'lt> is covariant (in 'lt) iff when 'a ⊇ 'b, T<'a> <: T<'b>

F<T> is covariant (in T) iff when T <: U, F<T> <: F<U>

danielhenrymantilla · 2022-02-25T16:55:26Z

src/subtyping.md


-Mr. Snuggles is a Cat, and Cats aren't *exactly* Animals, so we can't love him! 😿
+An example of simple subtyping that exists in the language are [supertraits](https://doc.rust-lang.org/stable/book/ch19-03-advanced-traits.html?highlight=supertraits#using-supertraits-to-require-one-traits-functionality-within-another-trait)


Ugh, I don't like at all the idea of conflating super-traits with sub(,super)-types: traits are not types; so the one thing that could make sense to connect stuff would be that when given trait A : B {}, a dyn A can coerce (≠ subtype!) to a dyn B. But since the root is about traits ≠ types, and involvesdyn and coercions, I'd very much keep the mention to trait hierarchy to its own separate chapter, lest people learning conflate stuff ⚠️

On the other hand, better detailing all the interactions stemming from trait hierarchy, when done within its own chapter, would be also very much appreciated 🙂

src/subtyping.md

danielhenrymantilla · 2022-02-25T17:08:13Z

src/subtyping.md

+Let's define a lifetime to be the simple requirement:
+`'a` defines a region of code in which a value will be alive.
+Now that we have a defined set of requirements for lifetimes, we can define how they relate to each other.
+`'long: 'short` if and only if `'long` defines a region of code that **completely contains** `'short`.


Suggested change

`'long: 'short` if and only if `'long` defines a region of code that **completely contains** `'short`.

`'long : 'short` if and only if `'long` defines a region of code that **completely contains** `'short` (_i.e._, `'long ⊇ 'short`)

I've added the whitespace to 'a : 'b kind of bounds, since we're not really within rustfmt-ed code anymore, we're teaching stuff, and : for lifetimes represents an (antisymmetrical) binary "boolean" operator, so there is no reason to favor the left hand side over the right hand side.

danielhenrymantilla · 2022-02-25T17:10:08Z

src/subtyping.md

+> But this is the Rustonomicon. We're writing unsafe code,
+so we need to understand how this stuff really works, and how we can mess it up.
+
+Going back to our example above, we can say that `'static: 'b`.


Suggested change

Going back to our example above, we can say that `'static: 'b`.

Going back to our example above, we can say that `'static : 'b`, as mentioned just above.

or, if my previous suggestions were not to be added:

Suggested change

Going back to our example above, we can say that `'static: 'b`.

Going back to our example above, we can say that `'static: 'b`. Indeed `'static` stands for `'forever`: the never-ending / infinite region. Since any other region is then thus contained within it (`'static ⊇ 'b`), we have `'static : 'b` for any lifetime `'b`.

src/subtyping.md

danielhenrymantilla · 2022-02-25T17:32:49Z

src/subtyping.md


-Variance is a property that *type constructors* have with respect to their
-arguments. A type constructor in Rust is any generic type with unbound arguments.
+Variance is the way that Rust defines the relationships of subtypes through their *type constructor*.


Could we avoid type constructors and talk of generic types instead? It ought to be clearer. Moreover, it incidentally allows to add the sentence: talking of the variance of a non-generic type makes no sense.

We're glossing over for<'any> fn(&'any str) <: fn(&'concrete str) here, by the way, but I think that's fine

danielhenrymantilla · 2022-02-25T17:36:14Z

src/subtyping.md


-If `F` has multiple type parameters, we can talk about the individual variances
-by saying that, for example, `F<T, U>` is covariant over `T` and invariant over `U`.
+If we remember from the above examples,


FWIW, I agree with @conradludgate's point about the advantage of using : everywhere; it allows to use this "subtyping is passed through" / "subtyping is inverted" wave-handed but very useful mnemonic.

It may also be useful to draw a tangential (footnote?) parallel with function monotonicity in mathematics, since for those that know that notion they can suddenly realize they know what all this is all about 🙂

conradludgate · 2022-02-25T21:17:26Z

Thanks everyone for the reviews. It seems overall people are in favour of this general form but there's a bit of bike shedding over syntax.

I'll make all the grammatical and language changes suggested

src/subtyping.md

jackh726 · 2022-04-01T14:01:05Z

@conradludgate the types team (wg-traits on zulip) is planning to go over this PR next Friday at 9 am Eastern Time. You're welcome to join if you'd like!

nikomatsakis

Gave this a read. Some notes:

I didn't spot any errors, beyond a certain imprecision in distinguishing types/traits/lifetimes and their relationships.
I've not read the rest of the rustonomicon so I can't really comment on how consistent that usage is, but I think we are definitely going to have to change it eventually. In particular, I think it's we want to have a "sublifetime" relationship (let's write it <:_l for now). Even though 'a <:_l 'b iff 'a: 'b, that doesn't make outlives equivalent, because it's also valid to have an outlives relation between lifetimes and types (and even, in the work I've been doing lately, types and types).
That said, I'm not clear 100% on the goals of this book/chapter, so I don't know how much it makes sense to worry at this moment about the distinctions there.
What did seem to be missing from this chapter was a bit of practical advice: how do you (for example) write a test that variance is what you expect? You don't mention how the compiler infers variance and the fact that it has associated semver/soundness implications, but that seems important.

src/subtyping.md

lcnr

a few nits, then r=me.

there are also some other open reviews you may want to deal with before merging

lcnr · 2022-06-20T10:39:50Z

src/subtyping.md

 }
 ```

-But unlike normal traits, we can use them as concrete and sized types, just like structs.
+In a conservative implementation of lifetimes, since `hello` and `world` have differing lifetimes,


Suggested change

In a conservative implementation of lifetimes, since `hello` and `world` have differing lifetimes,

In a conservative implementation of lifetimes, since `hello` and `world` have different lifetimes,

or distinct? 🤷 differing feels a bit weird to me

lcnr · 2022-06-20T10:42:37Z

src/subtyping.md

+Going back to our example above, we can say that `'static <: 'world`.
+For now, let's also accept the idea that subtypes of lifetimes can be passed through references
+(more on this in [Variance](#variance)),
+_e.g._ `&'static str` is a subtype of `&'world str`, then we can let a `&'static str` "downgrade" into a `&'world str`.


Suggested change

_e.g._ `&'static str` is a subtype of `&'world str`, then we can let a `&'static str` "downgrade" into a `&'world str`.

_e.g._ `&'static str` is a subtype of `&'world str`, then we can "downgrade" `&'static str` into a `&'world str`.

lcnr · 2022-06-20T10:45:36Z

src/subtyping.md

+With that, the example above will compile:
+
+```rust
+fn debug<T: std::fmt::Debug>(a: T, b: T) {


Suggested change

fn debug<T: std::fmt::Debug>(a: T, b: T) {

fn debug<'a>(a: &'a str, b: &'a str) {

to stay consistent with the original example

lcnr · 2022-06-20T10:49:57Z

src/subtyping.md

-adopts a constraint: `&'spike_str str` must be a subtype of `&'static str` (inclusive),
-which in turn implies `'spike_str` must be a subtype of `'static` (inclusive). Which is to say,
-`'spike_str` must contain `'static`. But only one thing contains `'static` -- `'static` itself!
+This is counter to the `&T` case:


there is no & here?

Maybe actually stay with &'a str instead of using some type parameter T here

lcnr · 2022-06-20T10:51:59Z

src/subtyping.md

@@ -197,116 +174,45 @@ For more types, see the ["Variance" section][variance-table] on the reference.
 > take references with specific lifetimes (as opposed to the usual "any lifetime",
 > which gets into higher rank lifetimes, which work independently of subtyping).


that's just wrong, higher rank lifetimes don't work independently of subtyping.

you don't have to fix that here as it's an existing issue

jyn514 · 2023-02-08T21:12:55Z

oof, it's been a while ... what's the current state of this PR?

I would prefer to merge this even if it's not 100% complete rather than have it hang in limbo; we can always improve it in follow-ups and my understand is it's already more accurate than the existing docs.

replace subtyping syntax remove type constructors

ehuss

Thanks @conradludgate for working on this!

I went through and applied some of the review suggestions. If anyone has anything more specific that they would like to see, feel free to open a new PR to update this.

Update books ## nomicon 2 commits in b5f018fb5930cb733b0a8aaf2eed975d4771e74d..c369e4b489332f8721fbae630354fa83385d457d 2023-05-19 11:10:25 -0700 to 2023-06-04 23:21:07 +0900 - phantom-data: Add `Send` and `Sync` columns (rust-lang/nomicon#411) - Rewrite the chapter on subtyping and variance (rust-lang/nomicon#340) ## reference 5 commits in 553d99b02a53b4133a40d5bd2e19958c67487c00..5ca365eac678cb0d41a20b3204546d6ed70c7171 2023-05-22 10:50:07 -0700 to 2023-06-22 10:13:08 -0700 - Document the ordering behavior of crate cfgs (rust-lang/reference#1369) - fix incorrect syntax for type-paths (rust-lang/reference#1370) - Fix inconsistent formatting of Disambiguating Function Calls example (rust-lang/reference#1366) - Add LoongArch to inline-assembly documentation (rust-lang/reference#1357) - comments: Fix typo: inner -> outer (rust-lang/reference#1364) ## book 1 commits in 8fa6b854d515506d825390fe0d817f5ef0c89350..21cf840842bdf768a798869f06373c96c1cc5122 2023-04-12 20:05:30 -0400 to 2023-06-12 12:24:06 -0400 - Correct `i32` formatting in ch19-05 ## rust-by-example 10 commits in 8ee9528b72b927cff8fd32346db8bbd1198816f0..57636d6926762861f34e030d52ca25a71e95e5bf 2023-05-01 18:18:34 -0300 to 2023-06-20 21:49:11 -0300 - Fixed line number (rust-lang/rust-by-example#1723) - Fix example in from_into.md (rust-lang/rust-by-example#1720) - cast.md improvements for signed boundary case casting (rust-lang/rust-by-example#1719) - Correct commentary about arrays in iter_find.md (rust-lang/rust-by-example#1714) - Improved wording in asm.md (rust-lang/rust-by-example#1717) - fix link to inline assembly reference (rust-lang/rust-by-example#1715) - Fix grammar in string.md (rust-lang/rust-by-example#1713) - Update let-else example with main function (rust-lang/rust-by-example#1711) - Expand `Option::and_then` example to contrast with `map` (rust-lang/rust-by-example#1710) - Add example for destructuring structs without match (rust-lang/rust-by-example#1709) ## rustc-dev-guide 9 commits in f1e637883fafeb83bdd5906ee7f467e4d35b7337..17fe3e948498c50e208047a750f17d6a8d89669b 2023-05-17 21:44:05 -0500 to 2023-06-26 18:34:26 +0200 - fix_typo - run-make tests: fix and improve (rust-lang/rustc-dev-guide#1702) - add stub for proof trees (rust-lang/rustc-dev-guide#1700) - Update track_caller reference link (rust-lang/rustc-dev-guide#1688) - Include information about setup defaults in how-to-build guide (rust-lang/rustc-dev-guide#1694) - Fix typo (rust-lang/rustc-dev-guide#1697) - Fix typo in thir.md - Update triagebot links. - name-resolution: Fix some typos in "Scopes and ribs"

conradludgate changed the title ~~Rewrite the chapter on subtyping~~ Rewrite the chapter on subtyping and variance Feb 10, 2022

T-Dark0 reviewed Feb 10, 2022

View reviewed changes

Noratrieb reviewed Feb 10, 2022

View reviewed changes

mejrs reviewed Feb 10, 2022

View reviewed changes

src/subtyping.md Outdated Show resolved Hide resolved

src/subtyping.md Outdated Show resolved Hide resolved

src/subtyping.md Outdated Show resolved Hide resolved

src/subtyping.md Outdated Show resolved Hide resolved

conradludgate marked this pull request as ready for review February 23, 2022 16:18

nrc reviewed Feb 24, 2022

View reviewed changes

LegionMammal978 reviewed Feb 24, 2022

View reviewed changes