work on traits chapters #70

nikomatsakis · Mar 2, 2018

This work begins to document the new-style trait solving system. This is documenting code that doesn't really exist yet -- my goal is to have the rustc-guide serve as a sort of living design document that we keep updating.

mark-i-m · Mar 2, 2018

Thanks again @nikomatsakis! Perhaps we have enough to make a traits/ subdirectory in the repo?

I will take a deeper dive soon.

nikomatsakis · Mar 6, 2018

@mark-i-m I could make a traits directory if you like. Also, I'm sort of inclined to land these without much review and keep iterating, since I want them to be easily accessible to people (i.e., easy for people to read).

nikomatsakis · Mar 6, 2018

I think I initially removed the directories for other pages because I found that I was shuffling around the "groups" sometimes -- i.e., creating or removing "subchapters" -- and I wanted to be able to have "more stable" URLs (in many cases, the file name still made sense, even if it was no longer a subdirectory). Those concerns may not apply here.

nikomatsakis · Mar 6, 2018

Splitting into directories proved harder than expected. I got weird errors from mdbook. Going to leave it for now.

mark-i-m · Mar 7, 2018

@nikomatsakis Sorry for the delay. Things have been busy... I had actually started reviewing. I think there are some places in this chapter where the uninitiate (like me 😛) would have a hard time following. If you want, I can try to move my review comments to an issue or something, but frankly, on GH, it's a lot easier to leave comments on a PR than on raw code... your call.

Splitting into directories proved harder than expected. I got weird errors from mdbook. Going to leave it for now.

That's fine. Thanks anyway :D

nikomatsakis · Mar 7, 2018

rebased, pushed an updated chapter

nikomatsakis · Mar 7, 2018

@scalexm I realized along the way that I don't know how implied bounds for GATs ought to work. I left some XXX in the chapter on lowering rules at the point of my confusion.

nikomatsakis · Mar 7, 2018

nikomatsakis reviewed Mar 7, 2018

View changes

nikomatsakis · Mar 7, 2018

src/traits-lowering-rules.md

+elsewhere.
+
+    // XXX how exactly should we set this up? Have to be careful;
+    // presumably this has to be a kind of `FromEnv` setup.


@scalexm here =)

nikomatsakis · Mar 7, 2018

@mark-i-m

frankly, on GH, it's a lot easier to leave comments on a PR than on raw code...

Yeah, totally. I guess we can leave it this way for a bit longer. The text is approaching "code complete" status.

mark-i-m · Mar 8, 2018

mark-i-m requested changes Mar 8, 2018

View changes

Thanks for your patience @nikomatsakis! I left a bunch of comments. Overall, I think this is very well-written.

I think the canonicalization section was the hardest for me to follow and fit into the system. I left a number of more detailed comments there.

Also, I had one more question: how do const-generics fit in? I'm assuming they are basically just another kind, but other than that everything is the same?

Thanks again!

mark-i-m · Mar 8, 2018

src/SUMMARY.md

@@ -17,10 +17,16 @@
 - [The HIR (High-level IR)](./hir.md)
 - [The `ty` module: representing types](./ty.md)
 - [Type inference](./type-inference.md)
- [Trait resolution](./trait-resolution.md)
+- [Trait bsolving (old-style)](./trait-resolution.md)


mark-i-m · Mar 8, 2018

src/trait-resolution.md

+**Note:** This chapter (and its subchapters) describe how the trait
+solver **currently** works. However, we are in the process of
+designing a new trait solver. If you'd prefer to read about *that*,
+see [the traits chapter](./traits.html).


s/the traits chapter/_this_ traits chapter/

mark-i-m · Mar 8, 2018

src/traits.md

+the process of being implemented; this chapter serves as a kind of
+in-progress design document. If you would prefer to read about how the
+current trait solver works, check out
+[this chapter](./trait-resolution.html).🚧


Perhaps add a link to the tracking issue for the new solver?

mark-i-m · Mar 8, 2018

src/traits-canonicalization.md

+[inference variable](./type-inference.html#vars) is always in one of two
+states: either it is **unbound**, in which case we don't know yet what
+type it is, or it is **bound**, in which case we do. So to isolate
+some thing T from its environment, we just walk down and find the


Perhaps use a more precise word than "thing"?

mark-i-m · Mar 8, 2018

src/traits-canonicalization.md

+a canonical order (left to right, for the most part, but really it
+doesn't matter as long as it is consistent).
+
+So, for example, if we have the type `X = (?T, ?U)`, where `?T` and


You may want to introduce the existential ? before this?

hmm. I sort of do, by saying "where ?T are inference variables", but it does feel like there is some missing introductory material. And maybe a notation section. I have to mull on this.

mark-i-m · Mar 8, 2018

src/traits-lowering-rules.md

+    forall<Self, P1..Pn, Pn+1..Pm> {
+      ProjectionEq(
+        <Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> =
+          (Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>


skolemized associated type projections are not introduced until the next chapter

I added more forward refs

mark-i-m · Mar 8, 2018

src/traits-lowering-rules.md

+
+The next rule covers implied bounds for the projection. In particular,
+the `Bounds` declared on the associated type must be proven to hold to
+show that the impl is well-formed, and hence we can rely on them from


s/from elsewhere/elsewhere/

mark-i-m · Mar 8, 2018

src/traits-lowering-rules.md

+impl<P0..Pn> Trait<A1..An> for A0
+where WC
+{
+    type AssocType<Pn+1..Pm>: Bounds where WC1 = T;


Um... do we generally have the bounds on the impl? Or is it here for pedagogy?

Oh, good...point

no I was just conflating trait + impl somehow

mark-i-m · Mar 8, 2018

src/traits-lowering-rules.md

@@ -0,0 +1,267 @@
+# Lowering rules


Overall this is pretty accessible, but there are a few places where Normalize is used, and it isn't really defined until a later section.

it might be that this should move until after both of them; this is sort of a "reference" section

I reorganized a bit

mark-i-m · Mar 8, 2018

src/traits-lowering-rules.md

+will create the following rules:
+
+    forall<P0..Pn> {
+      Implemented(TraitRef) :- WC


I'm assuming that if there is no where clause, WC is Top of something like that?

yeah... "true"

mark-i-m · Mar 8, 2018

Note that GH is hiding 23 comments again...

scalexm · Mar 8, 2018

scalexm reviewed Mar 8, 2018

View changes

scalexm · Mar 8, 2018

src/traits-lowering-to-logic.md

+
+Ok, so far so good. Let's move on to type-checking a more complex function.
+
+## Type-checking generic functions: beyond Horn clauses


Maybe add an example of implied bounds "in practice" in this section, where we in fact assume FromEnv(T: Eq) when type-checking the function below.

hmm I think we want to add a new "implied bounds" section -- beyond what's there now -- that kind of explains in a more "conversational" style. I'll add a placeholder for now, I'm sick of editing.

nikomatsakis · Mar 10, 2018

Ok, did some massive restructuring in response to @mark-i-m's feedback.

nikomatsakis · Mar 10, 2018

OK, I'm going to merge this -- but feel free to leave more comments and I will address.

mark-i-m · Mar 12, 2018

mark-i-m reviewed Mar 12, 2018

View changes

mark-i-m · Mar 12, 2018

src/traits-canonicalization.md

+
+    Canonical(QR) = for<T, L> {
+      certainty: Proven,
+      var_values: [Vec<?0>, '?1, ?2]


Should ?2 be ?0 here? Same in region constraints?

mark-i-m · Mar 12, 2018

mark-i-m reviewed Mar 12, 2018

View changes

mark-i-m · Mar 12, 2018

src/traits-canonicalization.md

+
+    for<T, L> {
+      certainty: Proven,
+      var_values: [Vec<?0>, '?1, ?2]


Same here...

nikomatsakis force-pushed the nikomatsakis:traits branch 2 times, most recently from 0a1af6f to 901e533 Mar 7, 2018

nikomatsakis force-pushed the nikomatsakis:traits branch from 901e533 to 5534f06 Mar 7, 2018

nikomatsakis force-pushed the nikomatsakis:traits branch from 5534f06 to 5fe3bc9 Mar 7, 2018

nikomatsakis referenced this pull request Mar 8, 2018
Closed
master tracking issue #6
11 of 20 tasks complete

nikomatsakis force-pushed the nikomatsakis:traits branch from 5fe3bc9 to 7a78a99 Mar 10, 2018

nikomatsakis added some commits Mar 10, 2018

fix link

Loading status checks…

d9f0a45

trailing whitespace

Loading status checks…

49e8e09

nikomatsakis merged commit c207e4c into rust-lang:master Mar 10, 2018
1 check passed

1 check passed

continuous-integration/travis-ci/pr The Travis CI build passed
Details

rust-lang/rustc-guide

Join GitHub today

work on traits chapters #70

Conversation

nikomatsakis commented Mar 2, 2018

This comment has been minimized.

mark-i-m commented Mar 2, 2018

This comment has been minimized.

nikomatsakis commented Mar 6, 2018

This comment has been minimized.

nikomatsakis commented Mar 6, 2018

This comment has been minimized.

nikomatsakis commented Mar 6, 2018

This comment has been minimized.

mark-i-m commented Mar 7, 2018

nikomatsakis force-pushed the nikomatsakis:traits branch 2 times, most recently from 0a1af6f to 901e533 Mar 7, 2018

This comment has been minimized.

nikomatsakis commented Mar 7, 2018

nikomatsakis force-pushed the nikomatsakis:traits branch from 901e533 to 5534f06 Mar 7, 2018

This comment has been minimized.

nikomatsakis commented Mar 7, 2018

nikomatsakis force-pushed the nikomatsakis:traits branch from 5534f06 to 5fe3bc9 Mar 7, 2018

nikomatsakis reviewed Mar 7, 2018 View changes

This comment has been minimized.

This comment has been minimized.

nikomatsakis commented Mar 7, 2018

mark-i-m requested changes Mar 8, 2018 View changes

mark-i-m left a comment

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

mark-i-m commented Mar 8, 2018

nikomatsakis referenced this pull request Mar 8, 2018

scalexm reviewed Mar 8, 2018 View changes

This comment has been minimized.

This comment has been minimized.

nikomatsakis force-pushed the nikomatsakis:traits branch from 5fe3bc9 to 7a78a99 Mar 10, 2018

This comment has been minimized.

nikomatsakis commented Mar 10, 2018

nikomatsakis added some commits Feb 27, 2018

nikomatsakis added some commits Mar 10, 2018

This comment has been minimized.

nikomatsakis commented Mar 10, 2018

Hide details View details nikomatsakis merged commit c207e4c into rust-lang:master Mar 10, 2018 1 check passed

1 check passed

mark-i-m reviewed Mar 12, 2018 View changes

This comment has been minimized.

mark-i-m reviewed Mar 12, 2018 View changes

This comment has been minimized.

nikomatsakis force-pushed the nikomatsakis:traits branch 2 times, most recently from `0a1af6f` to `901e533` Mar 7, 2018

nikomatsakis force-pushed the nikomatsakis:traits branch from `901e533` to `5534f06` Mar 7, 2018

nikomatsakis force-pushed the nikomatsakis:traits branch from `5534f06` to `5fe3bc9` Mar 7, 2018

nikomatsakis reviewed Mar 7, 2018

View changes

mark-i-m requested changes Mar 8, 2018

View changes

scalexm reviewed Mar 8, 2018

View changes

nikomatsakis force-pushed the nikomatsakis:traits branch from `5fe3bc9` to `7a78a99` Mar 10, 2018

nikomatsakis merged commit `c207e4c` into rust-lang:master Mar 10, 2018
1 check passed

mark-i-m reviewed Mar 12, 2018

View changes

mark-i-m reviewed Mar 12, 2018

View changes