Polish lowering chapters and update rules
This commit is contained in:
scalexm
Who? Me?!
parent
70b91d54a5
commit
cd3afd5ed6
|
|
@ -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<T: IntoIterator>(...) { ... }
|
|||
|
||||
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)<T>`. You
|
||||
may note that it looks a lot like a regular type (e.g., `Option<T>`),
|
||||
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<T>` 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(<T as IntoIterator>::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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
<a name="domain-goals"></a>
|
||||
|
||||
## 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<K1, ..., Kn> { 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.
|
||||
|
||||
<a name="trait-ref"></a>
|
||||
|
||||
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 = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
|
|||
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<i32>)`
|
||||
|
||||
e.g. `FromEnv(<Self as StreamingIterator>::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<K>)`
|
||||
|
||||
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<K> where K: Hash { ... }
|
||||
|
||||
fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
|
||||
println!("inserting!");
|
||||
set.insert(item);
|
||||
}
|
||||
```
|
||||
|
||||
`HashSet<K>` is an input type of the `loud_insert` function. Hence, we assume it
|
||||
to be well-formed, so we would have `FromEnv(HashSet<K>)` inside the body or our
|
||||
function. As we'll see in the section on lowering, `FromEnv(HashSet<K>)` 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<i32>)`, which is true in Rust, or
|
||||
* *Types*, like `WellFormed(Vec<i32>)`, which is true in Rust, or
|
||||
`WellFormed(Vec<str>)`, which is not (because `str` is not `Sized`.)
|
||||
|
||||
**TraitRefs**, like `WellFormed(Vec<i32>: Clone)`.
|
||||
|
||||
**Projections**, like `WellFormed(T: Iterator<Item = u32>)`.
|
||||
* *TraitRefs*, like `WellFormed(Vec<i32>: 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<K>)` in the `loud_insert`
|
||||
example because we will verify `WellFormed(HashSet<K>)` for each call site of
|
||||
`loud_insert`.
|
||||
|
||||
#### Outlives(Type: Region), Outlives(Region: Region)
|
||||
e.g. `Outlives(&'a str: 'b)`, `Outlives('a: 'static)`
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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<A1..An>` maps to `Implemented(A0: Foo<A1..An>)`.
|
||||
- `A0: Foo<A1..An, Item = T>` maps to
|
||||
`ProjectionEq(<A0 as Foo<A1..An>>::Item = T)`
|
||||
- `A0: Foo<A1..An>` maps to `Implemented(A0: Foo<A1..An>)`
|
||||
- `T: 'r` maps to `Outlives(T, 'r)`
|
||||
- `'a: 'b` maps to `Outlives('a, 'b)`
|
||||
- `A0: Foo<A1..An, Item = T>` is a bit special and expands to two distinct
|
||||
goals, namely `Implemented(A0: Foo<A1..An>)` and
|
||||
`ProjectionEq(<A0 as Foo<A1..An>>::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<Self, P1..Pn> {
|
|||
#### 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<P1..Pn> {
|
||||
|
|
@ -280,10 +286,10 @@ forall<Self, P1..Pn, Pn+1..Pm, U> {
|
|||
```
|
||||
|
||||
```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<Self, P1..Pn, Pn+1..Pm> {
|
||||
ProjectionEq(
|
||||
<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> =
|
||||
|
|
@ -303,7 +309,7 @@ elsewhere.
|
|||
// For each `Bound` in `Bounds`:
|
||||
forall<Self, P1..Pn, Pn+1..Pm> {
|
||||
FromEnv(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm>>: Bound) :-
|
||||
FromEnv(Self: Trait<P1..Pn>)
|
||||
FromEnv(Self: Trait<P1..Pn>) && WC1
|
||||
}
|
||||
```
|
||||
|
||||
|
|
@ -314,7 +320,7 @@ type to be well-formed...
|
|||
// Rule WellFormed-AssocTy
|
||||
forall<Self, P1..Pn, Pn+1..Pm> {
|
||||
WellFormed((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>) :-
|
||||
WC1, Implemented(Self: Trait<P1..Pn>)
|
||||
Implemented(Self: Trait<P1..Pn>) && WC1
|
||||
}
|
||||
```
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue