From 5c67241e1ab4383035cec2a0faa17c97ae51c007 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Wed, 24 Oct 2018 21:15:11 -0500 Subject: [PATCH 1/8] Group logic-related things under one section I found the layout to be a bit inconsistent before. This groups anything that touches logic rules under "Lowering to logic". This might be crowding too many things under that section, but it makes more sense to me overall. --- src/SUMMARY.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 213a645ab..9308b7d51 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -38,12 +38,12 @@ - [Goals and clauses](./traits/goals-and-clauses.md) - [Equality and associated types](./traits/associated-types.md) - [Implied bounds](./traits/implied-bounds.md) + - [Well-formedness checking](./traits/wf.md) - [Region constraints](./traits/regions.md) + - [The lowering module in rustc](./traits/lowering-module.md) + - [Lowering rules](./traits/lowering-rules.md) - [Canonical queries](./traits/canonical-queries.md) - [Canonicalization](./traits/canonicalization.md) - - [Lowering rules](./traits/lowering-rules.md) - - [The lowering module in rustc](./traits/lowering-module.md) - - [Well-formedness checking](./traits/wf.md) - [The SLG solver](./traits/slg.md) - [An Overview of Chalk](./traits/chalk-overview.md) - [Bibliography](./traits/bibliography.md) From 9ae8422607397558bd3d397ac3c01a915db24c56 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Wed, 24 Oct 2018 21:22:32 -0500 Subject: [PATCH 2/8] Reflect traits chapter structure in index key ideas --- src/traits/index.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/traits/index.md b/src/traits/index.md index 053a26bab..6a0e560a2 100644 --- a/src/traits/index.md +++ b/src/traits/index.md @@ -19,18 +19,18 @@ Trait solving is based around a few key ideas: describes the precise form of rules we use, and [lowering rules](./lowering-rules.html) gives the complete set of lowering rules in a more reference-like form. + - [Lazy normalization](./associated-types.html), which is the + technique we use to accommodate associated types when figuring out + whether types are equal. + - [Region constraints](./regions.html), which are accumulated + during trait solving but mostly ignored. This means that trait + solving effectively ignores the precise regions involved, always – + but we still remember the constraints on them so that those + constraints can be checked by the type checker. - [Canonical queries](./canonical-queries.html), which allow us to solve trait problems (like "is `Foo` implemented for the type `Bar`?") once, and then apply that same result independently in many different inference contexts. -- [Lazy normalization](./associated-types.html), which is the - technique we use to accommodate associated types when figuring out - whether types are equal. -- [Region constraints](./regions.html), which are accumulated - during trait solving but mostly ignored. This means that trait - solving effectively ignores the precise regions involved, always – - but we still remember the constraints on them so that those - constraints can be checked by thet type checker. Note: this is not a complete list of topics. See the sidebar for more. From c4708f8039f325b2f22cb4cc94744615e4529418 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Wed, 24 Oct 2018 21:22:57 -0500 Subject: [PATCH 3/8] Traits: Improve index layout, add chalk blurb --- src/traits/index.md | 51 +++++++++++++++++++++++++++++---------------- 1 file changed, 33 insertions(+), 18 deletions(-) diff --git a/src/traits/index.md b/src/traits/index.md index 6a0e560a2..2e3e6715c 100644 --- a/src/traits/index.md +++ b/src/traits/index.md @@ -1,17 +1,26 @@ # Trait solving (new-style) -🚧 This chapter describes "new-style" trait solving. This is still in the -[process of being implemented][wg]; 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 other chapter](./resolution.html). (By the way, if you -would like to help in hacking on the new solver, you will find -instructions for getting involved in the -[Traits Working Group tracking issue][wg].) 🚧 +> 🚧 This chapter describes "new-style" trait solving. This is still in the +> [process of being implemented][wg]; 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 other chapter](./resolution.html). 🚧 +> +> By the way, if you would like to help in hacking on the new solver, you will +> find instructions for getting involved in the +> [Traits Working Group tracking issue][wg]. [wg]: https://github.com/rust-lang/rust/issues/48416 -Trait solving is based around a few key ideas: +The new-style trait solver is based on the work done in [chalk][chalk]. Chalk +recasts Rust's trait system explicitly in terms of logic programming. It does +this by "lowering" Rust code into a kind of logic program we can then execute +queries against. + +You can read more about chalk itself in the +[Overview of Chalk](./chalk-overview.md) section. + +Trait solving in rustc is based around a few key ideas: - [Lowering to logic](./lowering-to-logic.html), which expresses Rust traits in terms of standard logical terms. @@ -32,17 +41,23 @@ Trait solving is based around a few key ideas: `Bar`?") once, and then apply that same result independently in many different inference contexts. -Note: this is not a complete list of topics. See the sidebar for more. +> This is not a complete list of topics. See the sidebar for more. +## Ongoing work The design of the new-style trait solving currently happens in two places: -* The [chalk][chalk] repository is where we experiment with new ideas and - designs for the trait system. It basically consists of a unit testing framework - for the correctness and feasibility of the logical rules defining the new-style - trait system. It also provides the [`chalk_engine`][chalk_engine] crate, which - defines the new-style trait solver used both in the unit testing framework and - in rustc. -* Once we are happy with the logical rules, we proceed to implementing them in - rustc. This mainly happens in [`librustc_traits`][librustc_traits]. + +**chalk**. The [chalk][chalk] repository is where we experiment with new ideas +and designs for the trait system. It primarily consists of two parts: +* a unit testing framework + for the correctness and feasibility of the logical rules defining the + new-style trait system. +* the [`chalk_engine`][chalk_engine] crate, which + defines the new-style trait solver used both in the unit testing framework + and in rustc. + +**rustc**. Once we are happy with the logical rules, we proceed to +implementing them in rustc. This mainly happens in +[`librustc_traits`][librustc_traits]. [chalk]: https://github.com/rust-lang-nursery/chalk [chalk_engine]: https://github.com/rust-lang-nursery/chalk/tree/master/chalk-engine From 99a23f84a7b1276ecc280da4ae4aba11f73f5edf Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Wed, 24 Oct 2018 21:31:53 -0500 Subject: [PATCH 4/8] Associated types: Mention "lazy normalization" somewhere --- src/traits/associated-types.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/traits/associated-types.md b/src/traits/associated-types.md index 1fffa3ff8..23da15228 100644 --- a/src/traits/associated-types.md +++ b/src/traits/associated-types.md @@ -5,7 +5,7 @@ associated types. The full system consists of several moving parts, which we will introduce one by one: - Projection and the `Normalize` predicate -- Skolemization +- Placeholder associated type projections - The `ProjectionEq` predicate - Integration with unification @@ -106,9 +106,10 @@ placeholder associated types (see the `TypeName` enum declared in So far we have seen two ways to answer the question of "When can we consider an associated type projection equal to another type?": -- the `Normalize` predicate could be used to transform associated type - projections when we knew which impl was applicable; -- **placeholder** associated types can be used when we don't. +- the `Normalize` predicate could be used to transform projections when we + knew which impl applied; +- **placeholder** associated types can be used when we don't. This is also + known as **lazy normalization**. We now introduce the `ProjectionEq` predicate to bring those two cases together. The `ProjectionEq` predicate looks like so: From fbb3ec6744e3a010f37e88c260949de6485575b8 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Wed, 24 Oct 2018 21:32:04 -0500 Subject: [PATCH 5/8] Associated types: Break up text for readability --- src/traits/associated-types.md | 59 +++++++++++++++++----------------- 1 file changed, 30 insertions(+), 29 deletions(-) diff --git a/src/traits/associated-types.md b/src/traits/associated-types.md index 23da15228..d35fb71e1 100644 --- a/src/traits/associated-types.md +++ b/src/traits/associated-types.md @@ -14,11 +14,11 @@ which we will introduce one by one: When a trait defines an associated type (e.g., [the `Item` type in the `IntoIterator` trait][intoiter-item]), that type can be referenced by the user using an **associated type -projection** like ` as IntoIterator>::Item`. (Often, -though, people will use the shorthand syntax `T::Item` – presently, -that syntax is expanded during -["type collection"](../type-checking.html) into the explicit form, -though that is something we may want to change in the future.) +projection** like ` as IntoIterator>::Item`. + +> Often, people will use the shorthand syntax `T::Item`. Presently, that +> syntax is expanded during ["type collection"](../type-checking.html) into the +> explicit form, though that is something we may want to change in the future. [intoiter-item]: https://doc.rust-lang.org/nightly/core/iter/trait.IntoIterator.html#associatedtype.Item @@ -41,10 +41,11 @@ IntoIterator>::Item` to just `u32`. In this case, the projection was a "monomorphic" one – that is, it did not have any type parameters. Monomorphic projections are special -because they can **always** be fully normalized – but often we can -normalize other associated type projections as well. For example, -` as IntoIterator>::Item` (where `?T` is an inference -variable) can be normalized to just `?T`. +because they can **always** be fully normalized. + +Often, we can normalize other associated type projections as well. For +example, ` as IntoIterator>::Item`, where `?T` is an inference +variable, can be normalized to just `?T`. In our logic, normalization is defined by a predicate `Normalize`. The `Normalize` clauses arise only from @@ -60,9 +61,8 @@ forall { where in this case, the one `Implemented` condition is always true. -(An aside: since we do not permit quantification over traits, this is -really more like a family of program clauses, one for each associated -type.) +> Since we do not permit quantification over traits, this is really more like +> a family of program clauses, one for each associated type. We could apply that rule to normalize either of the examples that we've seen so far. @@ -76,17 +76,18 @@ normalized. For example, consider this function: fn foo(...) { ... } ``` -In this context, how would we normalize the type `T::Item`? Without -knowing what `T` is, we can't really do so. To represent this case, we -introduce a type called a **placeholder associated type -projection**. This is written like so `(IntoIterator::Item)`. You -may note that it looks a lot like a regular type (e.g., `Option`), -except that the "name" of the type is `(IntoIterator::Item)`. This is -not an accident: placeholder associated type projections work just like -ordinary types like `Vec` when it comes to unification. That is, -they are only considered equal if (a) they are both references to the -same associated type, like `IntoIterator::Item` and (b) their type -arguments are equal. +In this context, how would we normalize the type `T::Item`? + +Without knowing what `T` is, we can't really do so. To represent this case, +we introduce a type called a **placeholder associated type projection**. This +is written like so: `(IntoIterator::Item)`. + +You may note that it looks a lot like a regular type (e.g., `Option`), +except that the "name" of the type is `(IntoIterator::Item)`. This is not an +accident: placeholder associated type projections work just like ordinary +types like `Vec` when it comes to unification. That is, they are only +considered equal if (a) they are both references to the same associated type, +like `IntoIterator::Item` and (b) their type arguments are equal. Placeholder associated types are never written directly by the user. They are used internally by the trait system only, as we will see @@ -152,16 +153,16 @@ might just fail, in which case we get back `Err(NoSolution)`. This would happen, for example, if we tried to unify `u32` and `i32`. The key point is that, on success, unification can also give back to -us a set of subgoals that still remain to be proven (it can also give +us a set of subgoals that still remain to be proven. (It can also give back region constraints, but those are not relevant here). -Whenever unification encounters an (un-placeholder!) associated type +Whenever unification encounters a non-placeholder associated type projection P being equated with some other type T, it always succeeds, but it produces a subgoal `ProjectionEq(P = T)` that is propagated back up. Thus it falls to the ordinary workings of the trait system to process that constraint. -(If we unify two projections P1 and P2, then unification produces a -variable X and asks us to prove that `ProjectionEq(P1 = X)` and -`ProjectionEq(P2 = X)`. That used to be needed in an older system to -prevent cycles; I rather doubt it still is. -nmatsakis) +> If we unify two projections P1 and P2, then unification produces a +> variable X and asks us to prove that `ProjectionEq(P1 = X)` and +> `ProjectionEq(P2 = X)`. (That used to be needed in an older system to +> prevent cycles; I rather doubt it still is. -nmatsakis) From c41019addab167642d743eebca4ce4a4a0865451 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Wed, 24 Oct 2018 21:24:53 -0500 Subject: [PATCH 6/8] Add status of regions --- src/traits/regions.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/traits/regions.md b/src/traits/regions.md index baa3582b6..4657529dc 100644 --- a/src/traits/regions.md +++ b/src/traits/regions.md @@ -1,3 +1,9 @@ # Region constraints -*to be written* +*To be written.* + +Chalk does not have the concept of region constraints, and as of this +writing, work on rustc was not far enough to worry about them. + +In the meantime, you can read about region constraints in the +[type inference](../type-inference.html#region-constraints) section. From 2de4dc7a12c2945454d958672c908b68d3495a75 Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Wed, 24 Oct 2018 21:30:33 -0500 Subject: [PATCH 7/8] Get excited --- src/traits/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/traits/index.md b/src/traits/index.md index 2e3e6715c..84f812394 100644 --- a/src/traits/index.md +++ b/src/traits/index.md @@ -8,7 +8,7 @@ > > By the way, if you would like to help in hacking on the new solver, you will > find instructions for getting involved in the -> [Traits Working Group tracking issue][wg]. +> [Traits Working Group tracking issue][wg]! [wg]: https://github.com/rust-lang/rust/issues/48416 From 74e2af231be0f1ff3350271b3624568c4244ef2d Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Fri, 26 Oct 2018 13:42:14 -0500 Subject: [PATCH 8/8] Put "well-formedness checking" under "lowering rules" This was also intended to be a reference chapter, according to @scalexm. --- src/SUMMARY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 9308b7d51..efe963c3f 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -38,10 +38,10 @@ - [Goals and clauses](./traits/goals-and-clauses.md) - [Equality and associated types](./traits/associated-types.md) - [Implied bounds](./traits/implied-bounds.md) - - [Well-formedness checking](./traits/wf.md) - [Region constraints](./traits/regions.md) - [The lowering module in rustc](./traits/lowering-module.md) - [Lowering rules](./traits/lowering-rules.md) + - [Well-formedness checking](./traits/wf.md) - [Canonical queries](./traits/canonical-queries.md) - [Canonicalization](./traits/canonicalization.md) - [The SLG solver](./traits/slg.md)