From e028ac2dc6977ac586f16c4450fe42f6560f34c8 Mon Sep 17 00:00:00 2001 From: scalexm Date: Tue, 16 Oct 2018 14:55:03 +0200 Subject: [PATCH 1/4] Polish lowering chapters and update rules --- src/traits/associated-types.md | 21 ++++++--- src/traits/goals-and-clauses.md | 84 ++++++++++++++++++++++++++------- src/traits/index.md | 14 ++++++ src/traits/lowering-rules.md | 36 ++++++++------ 4 files changed, 116 insertions(+), 39 deletions(-) diff --git a/src/traits/associated-types.md b/src/traits/associated-types.md index b8ac7f8b9..3330ce809 100644 --- a/src/traits/associated-types.md +++ b/src/traits/associated-types.md @@ -67,7 +67,7 @@ type.) We could apply that rule to normalize either of the examples that we've seen so far. -## Skolemized associated types +## Placeholder associated types Sometimes however we want to work with associated types that cannot be normalized. For example, consider this function: @@ -78,20 +78,29 @@ 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 **skolemized associated type +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: skolemized associated type projections work just like +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. -Skolemized associated types are never written directly by the user. +Placeholder associated types are never written directly by the user. They are used internally by the trait system only, as we will see shortly. +In rustc, they correspond to the `TyKind::UnnormalizedProjectionTy` enum +variant, declared in [`librustc/ty/sty.rs`][sty]. In chalk, we use an +`ApplicationTy` with a name living in a special namespace dedicated to +placeholder associated types (see the `TypeName` enum declared in +[`chalk-ir/src/lib.rs`][chalk_type_name]). + +[sty]: https://github.com/rust-lang/rust/blob/master/src/librustc/ty/sty.rs +[chalk_type_name]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-ir/src/lib.rs + ## Projection equality So far we have seen two ways to answer the question of "When can we @@ -99,7 +108,7 @@ 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; -- **skolemized** associated types can be used when we don't. +- **placeholder** associated types can be used when we don't. We now introduce the `ProjectionEq` predicate to bring those two cases together. The `ProjectionEq` predicate looks like so: @@ -109,7 +118,7 @@ ProjectionEq(::Item = U) ``` and we will see that it can be proven *either* via normalization or -skolemization. As part of lowering an associated type declaration from +via the placeholder type. As part of lowering an associated type declaration from some trait, we create two program clauses for `ProjectionEq`: ```text diff --git a/src/traits/goals-and-clauses.md b/src/traits/goals-and-clauses.md index 5aa3755ad..8cc1bc7fd 100644 --- a/src/traits/goals-and-clauses.md +++ b/src/traits/goals-and-clauses.md @@ -37,15 +37,33 @@ paper ["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf] gives the details. +In terms of code, these types are defined in +[`librustc/traits/mod.rs`][traits_mod] in rustc, and in +[`chalk-ir/src/lib.rs`][chalk_ir] in chalk. + [pphhf]: ./bibliography.html#pphhf +[traits_mod]: https://github.com/rust-lang/rust/blob/master/src/librustc/traits/mod.rs +[chalk_ir]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-ir/src/lib.rs ## Domain goals +*Domain goals* are the atoms of the trait logic. As can be seen in the +definitions given above, general goals basically consist in a combination of +domain goals. + +Moreover, flattenning a bit the definition of clauses given previously, one can +see that clauses are always of the form: +```text +forall { DomainGoal :- Goal } +``` +hence domain goals are in fact clauses LHS. That is, at the most granular level, +domain goals are what the trait solver will end up trying to prove. + -To define the set of *domain goals* in our system, we need to first +To define the set of domain goals in our system, we need to first introduce a few simple formulations. A **trait reference** consists of the name of a trait along with a suitable set of inputs P0..Pn: @@ -70,18 +88,24 @@ Projection = >::AssocItem Given these, we can define a `DomainGoal` as follows: ```text -DomainGoal = Implemented(TraitRef) - | ProjectionEq(Projection = Type) - | Normalize(Projection -> Type) +DomainGoal = Holds(WhereClause) | FromEnv(TraitRef) - | FromEnv(Projection = Type) - | WellFormed(Type) + | FromEnv(Type) | WellFormed(TraitRef) - | WellFormed(Projection = Type) + | WellFormed(Type) + | Normalize(Projection -> Type) + +WhereClause = Implemented(TraitRef) + | ProjectionEq(Projection = Type) | Outlives(Type: Region) | Outlives(Region: Region) ``` +`WhereClause` refers to a `where` clause that a Rust user would actually be able +to write in a Rust program. This abstraction exists only as a convenience as we +sometimes want to only coope with domain goals that are effectively writable in +Rust. + Let's break down each one of these, one-by-one. #### Implemented(TraitRef) @@ -109,12 +133,10 @@ also requires proving `Implemented(T: Trait)`. [n]: ./associated-types.html#normalize [at]: ./associated-types.html -#### FromEnv(TraitRef), FromEnv(Projection = Type) +#### FromEnv(TraitRef) e.g. `FromEnv(Self: Add)` -e.g. `FromEnv(::Item<'a> = &'a [u8])` - -True if the inner `TraitRef` or projection equality is *assumed* to be true; +True if the inner `TraitRef` is *assumed* to be true, that is, if it can be derived from the in-scope where clauses. For example, given the following function: @@ -131,24 +153,50 @@ where clauses nest, so a function body inside an impl body inherits the impl body's where clauses, too. This and the next rule are used to implement [implied bounds]. As we'll see -in the section on lowering, `FromEnv(X)` implies `Implemented(X)`, but not -vice versa. This distinction is crucial to implied bounds. +in the section on lowering, `FromEnv(TraitRef)` implies `Implemented(TraitRef)`, +but not vice versa. This distinction is crucial to implied bounds. + +#### FromEnv(Type) +e.g. `FromEnv(HashSet)` + +True if the inner `Type` is *assumed* to be well-formed, that is, if it is an +input type of a function or an impl. + +For example, given the following code: + +```rust,ignore +struct HashSet where K: Hash { ... } + +fn loud_insert(set: &mut HashSet, item: K) { + println!("inserting!"); + set.insert(item); +} +``` + +`HashSet` is an input type of the `loud_insert` function. Hence, we assume it +to be well-formed, so we would have `FromEnv(HashSet)` inside the body or our +function. As we'll see in the section on lowering, `FromEnv(HashSet)` implies +`Implemented(K: Hash)` because the +`HashSet` declaration was written with a `K: Hash` where clause. Hence, we don't +need to repeat that bound on the `loud_insert` function: we rather automatically +assume that it is true. #### WellFormed(Item) These goals imply that the given item is *well-formed*. We can talk about different types of items being well-formed: -**Types**, like `WellFormed(Vec)`, which is true in Rust, or +* *Types*, like `WellFormed(Vec)`, which is true in Rust, or `WellFormed(Vec)`, which is not (because `str` is not `Sized`.) -**TraitRefs**, like `WellFormed(Vec: Clone)`. - -**Projections**, like `WellFormed(T: Iterator)`. +* *TraitRefs*, like `WellFormed(Vec: Clone)`. Well-formedness is important to [implied bounds]. In particular, the reason -it is okay to assume `FromEnv(T: Clone)` in the example above is that we +it is okay to assume `FromEnv(T: Clone)` in the `loud_clone` example is that we _also_ verify `WellFormed(T: Clone)` for each call site of `loud_clone`. +Similarly, it is okay to assume `FromEnv(HashSet)` in the `loud_insert` +example because we will verify `WellFormed(HashSet)` for each call site of +`loud_insert`. #### Outlives(Type: Region), Outlives(Region: Region) e.g. `Outlives(&'a str: 'b)`, `Outlives('a: 'static)` diff --git a/src/traits/index.md b/src/traits/index.md index c5afb280b..053a26bab 100644 --- a/src/traits/index.md +++ b/src/traits/index.md @@ -33,3 +33,17 @@ Trait solving is based around a few key ideas: constraints can be checked by thet type checker. Note: this is not a complete list of topics. See the sidebar for more. + +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]: https://github.com/rust-lang-nursery/chalk +[chalk_engine]: https://github.com/rust-lang-nursery/chalk/tree/master/chalk-engine +[librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits diff --git a/src/traits/lowering-rules.md b/src/traits/lowering-rules.md index 218164c0f..88a61ac4f 100644 --- a/src/traits/lowering-rules.md +++ b/src/traits/lowering-rules.md @@ -27,19 +27,24 @@ comment like so: // Rule Foo-Bar-Baz -you can also search through the `librustc_traits` crate in rustc -to find the corresponding rules from the implementation. +The reference implementation of these rules is to be found in +[`chalk/src/rules.rs`][chalk_rules]. They are also ported in rustc in the +[`librustc_traits`][librustc_traits] crate. + +[chalk_rules]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules.rs +[librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits ## Lowering where clauses When used in a goal position, where clauses can be mapped directly to -[domain goals][dg], as follows: +the `Holds` variant of [domain goals][dg], as follows: -- `A0: Foo` maps to `Implemented(A0: Foo)`. -- `A0: Foo` maps to - `ProjectionEq(>::Item = T)` +- `A0: Foo` maps to `Implemented(A0: Foo)` - `T: 'r` maps to `Outlives(T, 'r)` - `'a: 'b` maps to `Outlives('a, 'b)` +- `A0: Foo` is a bit special and expands to two distinct + goals, namely `Implemented(A0: Foo)` and + `ProjectionEq(>::Item = T)` In the rules below, we will use `WC` to indicate where clauses that appear in Rust syntax; we will then use the same `WC` to indicate @@ -54,11 +59,10 @@ on the lowered where clauses, as defined here: - `FromEnv(WC)` – this indicates that: - `Implemented(TraitRef)` becomes `FromEnv(TraitRef)` - - `ProjectionEq(Projection = Ty)` becomes `FromEnv(Projection = Ty)` - other where-clauses are left intact - `WellFormed(WC)` – this indicates that: - `Implemented(TraitRef)` becomes `WellFormed(TraitRef)` - - `ProjectionEq(Projection = Ty)` becomes `WellFormed(Projection = Ty)` + - other where-clauses are left intact *TODO*: I suspect that we want to alter the outlives relations too, but Chalk isn't modeling those right now. @@ -99,9 +103,11 @@ forall { #### Implied bounds The next few clauses have to do with implied bounds (see also -[RFC 2089]). For each trait, we produce two clauses: +[RFC 2089] and the [implied bounds][implied_bounds] chapter for a more in depth +cover). For each trait, we produce two clauses: [RFC 2089]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html +[implied_bounds]: ./implied-bounds.md ```text // Rule Implied-Bound-From-Trait @@ -210,7 +216,7 @@ well-formed, we can also assume that its where clauses hold. That is, we produce the following family of rules: ```text -// Rule FromEnv-Type +// Rule Implied-Bound-From-Type // // For each where clause `WC` forall { @@ -280,10 +286,10 @@ forall { ``` ```text -// Rule ProjectionEq-Skolemize +// Rule ProjectionEq-Placeholder // -// ProjectionEq can succeed by skolemizing, see "associated type" -// chapter for more: +// ProjectionEq can succeed through the placeholder associated type, +// see "associated type" chapter for more: forall { ProjectionEq( >::AssocType = @@ -303,7 +309,7 @@ elsewhere. // For each `Bound` in `Bounds`: forall { FromEnv(>::AssocType>: Bound) :- - FromEnv(Self: Trait) + FromEnv(Self: Trait) && WC1 } ``` @@ -314,7 +320,7 @@ type to be well-formed... // Rule WellFormed-AssocTy forall { WellFormed((Trait::AssocType)) :- - WC1, Implemented(Self: Trait) + Implemented(Self: Trait) && WC1 } ``` From 505dafa3094705e0d240e6e6aa12d42da5743aa3 Mon Sep 17 00:00:00 2001 From: Who? Me?! Date: Sun, 21 Oct 2018 18:05:32 +0200 Subject: [PATCH 2/4] Add an apostrophe Co-Authored-By: scalexm --- src/traits/goals-and-clauses.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/traits/goals-and-clauses.md b/src/traits/goals-and-clauses.md index 8cc1bc7fd..494ec5b85 100644 --- a/src/traits/goals-and-clauses.md +++ b/src/traits/goals-and-clauses.md @@ -58,7 +58,7 @@ see that clauses are always of the form: ```text forall { DomainGoal :- Goal } ``` -hence domain goals are in fact clauses LHS. That is, at the most granular level, +hence domain goals are in fact clauses' LHS. That is, at the most granular level, domain goals are what the trait solver will end up trying to prove. From 50c646ef2348b5a0a52b0332fc251cf74178bbd1 Mon Sep 17 00:00:00 2001 From: Who? Me?! Date: Sun, 21 Oct 2018 18:05:51 +0200 Subject: [PATCH 3/4] Fix typo Co-Authored-By: scalexm --- src/traits/goals-and-clauses.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/traits/goals-and-clauses.md b/src/traits/goals-and-clauses.md index 494ec5b85..fb12c5a41 100644 --- a/src/traits/goals-and-clauses.md +++ b/src/traits/goals-and-clauses.md @@ -174,7 +174,7 @@ fn loud_insert(set: &mut HashSet, item: K) { ``` `HashSet` is an input type of the `loud_insert` function. Hence, we assume it -to be well-formed, so we would have `FromEnv(HashSet)` inside the body or our +to be well-formed, so we would have `FromEnv(HashSet)` inside the body of our function. As we'll see in the section on lowering, `FromEnv(HashSet)` implies `Implemented(K: Hash)` because the `HashSet` declaration was written with a `K: Hash` where clause. Hence, we don't From b96bcc4b3e7de7d4e7997a78c8df7bb7d76b3215 Mon Sep 17 00:00:00 2001 From: scalexm Date: Sun, 21 Oct 2018 18:07:25 +0200 Subject: [PATCH 4/4] Change wording --- src/traits/goals-and-clauses.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/traits/goals-and-clauses.md b/src/traits/goals-and-clauses.md index fb12c5a41..8f1ffa488 100644 --- a/src/traits/goals-and-clauses.md +++ b/src/traits/goals-and-clauses.md @@ -103,7 +103,7 @@ WhereClause = Implemented(TraitRef) `WhereClause` refers to a `where` clause that a Rust user would actually be able to write in a Rust program. This abstraction exists only as a convenience as we -sometimes want to only coope with domain goals that are effectively writable in +sometimes want to only deal with domain goals that are effectively writable in Rust. Let's break down each one of these, one-by-one. @@ -117,8 +117,8 @@ True if the given trait is implemented for the given input types and lifetimes. e.g. `ProjectionEq::Item = u8` The given associated type `Projection` is equal to `Type`; this can be proved -with either normalization or using skolemized types. See [the section -on associated types](./associated-types.html). +with either normalization or using placeholder associated types. See +[the section on associated types](./associated-types.html). #### Normalize(Projection -> Type) e.g. `ProjectionEq::Item -> u8`