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..8f1ffa488 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 deal with domain goals that are effectively writable in +Rust. + Let's break down each one of these, one-by-one. #### Implemented(TraitRef) @@ -93,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` @@ -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 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 +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 } ```