work on traits chapters #70

nikomatsakis · 2018-03-02T10:52:13Z

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 · 2018-03-02T18:22:28Z

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

I will take a deeper dive soon.

nikomatsakis · 2018-03-06T10:04:59Z

@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 · 2018-03-06T10:05:58Z

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 · 2018-03-06T19:21:40Z

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

mark-i-m · 2018-03-07T00:39:18Z

@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 · 2018-03-07T14:54:45Z

rebased, pushed an updated chapter

nikomatsakis · 2018-03-07T14:58:14Z

@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 · 2018-03-07T14:58:44Z

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 · 2018-03-07T14:59:51Z

@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

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 · 2018-03-02T18:23:01Z

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 · 2018-03-02T18:24:04Z

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 · 2018-03-02T18:25:14Z

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 · 2018-03-02T18:37:01Z

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 · 2018-03-02T18:37:54Z

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 · 2018-03-08T00:00:42Z

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 · 2018-03-08T00:02:57Z

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 · 2018-03-08T00:11:25Z

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 · 2018-03-08T00:15:58Z

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 · 2018-03-08T00:16:07Z

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 · 2018-03-08T00:43:20Z

Note that GH is hiding 23 comments again...

scalexm · 2018-03-08T12:16:09Z

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 · 2018-03-10T12:05:52Z

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

nikomatsakis · 2018-03-10T12:13:28Z

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

mark-i-m · 2018-03-12T17:49:21Z

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 · 2018-03-12T17:50:28Z

src/traits-canonicalization.md

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


Same here...

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

nikomatsakis force-pushed the traits branch from 901e533 to 5534f06 Compare March 7, 2018 14:58

nikomatsakis force-pushed the traits branch from 5534f06 to 5fe3bc9 Compare March 7, 2018 14:58

nikomatsakis commented Mar 7, 2018

View reviewed changes

mark-i-m suggested changes Mar 8, 2018

View reviewed changes

nikomatsakis mentioned this pull request Mar 8, 2018

master tracking issue #6

Closed

20 tasks

scalexm reviewed Mar 8, 2018

View reviewed changes

nikomatsakis force-pushed the traits branch from 5fe3bc9 to 7a78a99 Compare March 10, 2018 12:05

nikomatsakis added 11 commits March 10, 2018 07:06

work on traits chapters

479d914

clarify how there are two traits chapters

e4aaa9c

link to traits working group tracking issue

6f99f12

don't say 'thing'

fd92491

expand reorder topic list slightly

3c8a827

add background material on trait queries

c3a3502

update for notation

22b5ec4

rework canon section substantially to spell out steps more clearly

5311531

numerous edits

95f9957

add implied bounds placeholder

7a78a99

update the summary landing page

994a38b

nikomatsakis added 2 commits March 10, 2018 07:10

fix link

d9f0a45

trailing whitespace

49e8e09

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

mark-i-m reviewed Mar 12, 2018

View reviewed changes

src/traits-canonicalization.md

for<T, L> {

certainty: Proven,

var_values: [Vec<?0>, '?1, ?2]

Copy link

Member

mark-i-m Mar 12, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here...

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

work on traits chapters #70

work on traits chapters #70

nikomatsakis commented Mar 2, 2018

mark-i-m commented Mar 2, 2018

nikomatsakis commented Mar 6, 2018

nikomatsakis commented Mar 6, 2018

nikomatsakis commented Mar 6, 2018

mark-i-m commented Mar 7, 2018

nikomatsakis commented Mar 7, 2018

nikomatsakis commented Mar 7, 2018

nikomatsakis Mar 7, 2018

nikomatsakis commented Mar 7, 2018

mark-i-m left a comment

mark-i-m Mar 2, 2018

mark-i-m Mar 2, 2018

mark-i-m Mar 2, 2018

mark-i-m Mar 2, 2018

mark-i-m Mar 2, 2018

nikomatsakis Mar 9, 2018

mark-i-m Mar 8, 2018

nikomatsakis Mar 10, 2018

mark-i-m Mar 8, 2018

mark-i-m Mar 8, 2018

nikomatsakis Mar 10, 2018

nikomatsakis Mar 10, 2018

mark-i-m Mar 8, 2018

nikomatsakis Mar 10, 2018

nikomatsakis Mar 10, 2018

mark-i-m Mar 8, 2018

nikomatsakis Mar 10, 2018

mark-i-m commented Mar 8, 2018

scalexm Mar 8, 2018

nikomatsakis Mar 10, 2018

nikomatsakis commented Mar 10, 2018

nikomatsakis commented Mar 10, 2018

mark-i-m Mar 12, 2018

mark-i-m Mar 12, 2018


		Ok, so far so good. Let's move on to type-checking a more complex function.

		## Type-checking generic functions: beyond Horn clauses

work on traits chapters #70

work on traits chapters #70

Conversation

nikomatsakis commented Mar 2, 2018

mark-i-m commented Mar 2, 2018

nikomatsakis commented Mar 6, 2018

nikomatsakis commented Mar 6, 2018

nikomatsakis commented Mar 6, 2018

mark-i-m commented Mar 7, 2018

nikomatsakis commented Mar 7, 2018

nikomatsakis commented Mar 7, 2018

Choose a reason for hiding this comment

nikomatsakis commented Mar 7, 2018

mark-i-m left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mark-i-m commented Mar 8, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis commented Mar 10, 2018

nikomatsakis commented Mar 10, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment