mirror
/
rustc-dev-guide
mirror of https://github.com/rust-lang/rustc-dev-guide.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

work on traits chapters

This commit is contained in:
Niko Matsakis 2018-02-27 05:50:43 -05:00
parent 86c5f6c9b4
commit 479d914ff0
12 changed files with 912 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/SUMMARY.md
View File

@ -17,10 +17,19 @@
- [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 solving (old-style)](./trait-resolution.md)
- [Higher-ranked trait bounds](./trait-hrtb.md)
- [Caching subtleties](./trait-caching.md)
- [Speciailization](./trait-specialization.md)
- [Specialization](./trait-specialization.md)
- [Trait solving (new-style)](./traits.md)
- [Canonicalization](./traits-canonicalization.md)
- [Lowering to logic](./traits-lowering-to-logic.md)
- [Goals and clauses](./traits-goals-and-clauses.md)
- [Lowering rules](./traits-lowering-rules.md)
- [Equality and associated types](./traits-associated-types.md)
- [Region constraints](./traits-regions.md)
- [Well-formedness checking](./traits-wf.md)
- [Bibliography](./traits-bibliography.md)
- [Type checking](./type-checking.md)
- [The MIR (Mid-level IR)](./mir.md)
- [MIR construction](./mir-construction.md)

7
src/trait-resolution.md
View File

@ -1,8 +1,13 @@
# Trait resolution
# Trait resolution (old-style)
This chapter describes the general process of _trait resolution_ and points out
some non-obvious things.
**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).
## Major concepts
Trait resolution is the process of pairing up an impl with each

143
src/traits-associated-types.md Normal file
View File

@ -0,0 +1,143 @@
# Equality and associated types
This section covers how the trait system handles equality between
associated types. The full system consists of several moving parts,
which we will introduce one by one:
- Projection and the `Normalize` predicate
- Skolemization
- The `ProjectionEq` predicate
- Integration with unification
## Associated type projection and normalization
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 `<Option<u32> 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.)
In some cases, associated type projections can be **normalized** --
that is, simplified -- based on the types given in an impl. So, to
continue with our example, the impl of `IntoIterator` for `Option<T>`
declares (among other things) that `Item = T`:
```rust
impl<T> IntoIterator for Option<T> {
type Item = T;
..
}
```
This means we can normalize the projection `<Option<u32> as
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,
`<Option<?T> 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
impls. For example, the `impl` of `IntoIterator` for `Option<T>` that
we saw above would be lowered to a program clause like so:
forall<T> {
Normalize(<Option<T> as IntoIterator>::Item -> T)
}
(An aside: since we do not permit quantification over traits, this is
really more like a family of predicates, one for each associated
type.)
We could apply that rule to normalize either of the examples that
we've seen so far.
## Skolemized associated types
Sometimes however we want to work with associated types that cannot be
normalized. For example, consider this function:
```rust
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
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
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.
They are used internally by the trait system only, as we will see
shortly.
## Projection equality
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;
- **skolemized** 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:
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
some trait, we create two program clauses for `ProjectionEq`:
forall<T, U> {
ProjectionEq(<T as IntoIterator>::Item = U) :-
Normalize(<T as IntoIterator>::Item -> U)
}
forall<T> {
ProjectionEq(<T as IntoIterator>::Item = (IntoIterator::Item)<T>)
}
These are the only two `ProjectionEq` program clauses we ever make for
any given associated item.
## Integration with unification
Now we are ready to discuss how associated type equality integrates
with unification. As described in the
[type inference](./type-inference.html) section, unification is
basically a procedure with a signature like this:
Unify(A, B) = Result<(Subgoals, RegionConstraints), NoSolution>
In other words, we try to unify two things A and B. That procedure
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
back region constraints, but those are not relevant here).
Whenever unification encounters an (unskolemized!) 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)

28
src/traits-bibliography.md Normal file
View File

@ -0,0 +1,28 @@
# Bibliography
If you'd like to read more background material, here are some
recommended texts and papers:
[Programming with Higher-order Logic][phl], by Dale Miller and Gopalan
Nadathur, covers the key concepts of Lambda prolog. Although it's a
slim little volume, it's the kind of book where you learn something
new every time you open it.
[phl]: https://www.amazon.com/Programming-Higher-Order-Logic-Dale-Miller/dp/052187940X
<a name=pphhf>
["A proof procedure for the logic of Hereditary Harrop formulas"][pphhf],
by Gopalan Nadathur. This paper covers the basics of universes,
environments, and Lambda Prolog-style proof search. Quite readable.
[pphhf]: https://dl.acm.org/citation.cfm?id=868380
<a name=slg>
["A new formulation of tabled resolution with delay"][nftrd], by
[Theresa Swift]. This paper gives a kind of abstract treatment of the
SLG formulation that is the basis for our on-demand solver.
[nftrd]: https://dl.acm.org/citation.cfm?id=651202
[ts]: http://www3.cs.stonybrook.edu/~tswift/

93
src/traits-canonicalization.md Normal file
View File

@ -0,0 +1,93 @@
# Canonicalization
Canonicalization is the process of **isolating** an inference value
from its context. It is really based on a very simple concept: every
[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
unbound variables that appear in T; those variables get renumbered in
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
`?U` are distinct, unbound inference variables, then the canonical
form of `X` would be `(?0, ?1)`, where `?0` and `?1` represent these
**canonical placeholders**. Note that the type `Y = (?U, ?T)` also
canonicalizes to `(?0, ?1)`. But the type `Z = (?T, ?T)` would
canonicalize to `(?0, ?0)` (as would `(?U, ?U)`). In other words, the
exact identity of the inference variables is not important -- unless
they are repeated.
We use this to improve caching as well as to detect cycles and other
things during trait resolution. Roughly speaking, the idea is that if
two trait queries have the same canonicalize form, then they will get
the same answer -- modulo the precise identities of the variables
involved.
To see how it works, imagine that we are asking to solve the following
trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound.
This query contains two unbound variables, but it also contains the
lifetime `'static`. The trait system generally ignores all lifetimes
and treats them equally, so when canonicalizing, we will *also*
replace any [free lifetime](./background.html#free-vs-bound) with a
canonical variable. Therefore, we get the following result:
?0: Foo<'?1, ?2>
Sometimes we write this differently, like so:
for<T,L,T> { ?0: Foo<'?1, ?2> }
This `for<>` gives some information about each of the canonical
variables within. In this case, I am saying that `?0` is a type
(`T`), `?1` is a lifetime (`L`), and `?2` is also a type (`T`). The
`canonicalize` method *also* gives back a `CanonicalVarValues` array
with the "original values" for each canonicalized variable:
[?A, 'static, ?B]
Now we do the query and get back some result R. As part of that
result, we'll have an array of values for the canonical inputs. For
example, the canonical result might be:
```
for<2> {
values = [ Vec<?0>, '1, ?0 ]
^^ ^^ ^^ these are variables in the result!
...
}
```
Note that this result is itself canonical and may include some
variables (in this case, `?0`).
What we want to do conceptually is to (a) instantiate each of the
canonical variables in the result with a fresh inference variable
and then (b) unify the values in the result with the original values.
Doing step (a) would yield a result of
```
{
values = [ Vec<?C>, '?X, ?C ]
^^ ^^^ fresh inference variables in `self`
..
}
```
Step (b) would then unify:
```
?A with Vec<?C>
'static with '?X
?B with ?C
```
(What we actually do is a mildly optimized variant of that: Rather
than eagerly instantiating all of the canonical values in the result
with variables, we instead walk the vector of values, looking for
cases where the value is just a canonical variable. In our example,
`values[2]` is `?C`, so that we means we can deduce that `?C := ?B and
`'?X := 'static`. This gives us a partial set of values. Anything for
which we do not find a value, we create an inference variable.)

148
src/traits-goals-and-clauses.md Normal file
View File

@ -0,0 +1,148 @@
# Goals and clauses
In logic programming terms, a **goal** is something that you must
prove and a **clause** is something that you know is true. As
described in the [lowering to logic](./traits-lowering-to-logic.html)
chapter, Rust's trait solver is based on an extension of hereditary
harrop (HH) clauses, which extend traditional Prolog Horn clauses with
a few new superpowers.
## Goals and clauses meta structure
In Rust's solver, **goals** and **clauses** have the following forms
(note that the two definitions reference one another):
Goal = DomainGoal
| Goal && Goal
| Goal || Goal
| exists<K> { Goal } // existential quantification
| forall<K> { Goal } // universal quantification
| if (Clause) { Goal } // implication
Clause = DomainGoal
| Clause :- Goal // if can prove Goal, then Clause is true
| Clause && Clause
| forall<K> { Clause }
K = <type> // a "kind"
| <lifetime>
The proof procedure for these sorts of goals is actually quite
straightforward. Essentially, it's a form of depth-first search. The
paper
["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
gives the details.
[pphhf]: ./traits-bibliography.html#pphhf
<a name="domain-goals">
## Domain goals
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 allow with a suitable set of inputs P0..Pn:
TraitRef = P0: TraitName<P1..Pn>
So, for example, `u32: Display` is a trait reference, as is `Vec<T>:
IntoIterator`. Note that Rust surface syntax also permits some extra
things, like associated type bindings (`Vec<T>: IntoIterator<Item =
T>`), that are not part of a trait reference.
A **projection** consists of a an associated item reference along with
its inputs P0..Pm:
Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
Given that, we can define a `DomainGoal` as follows:
DomainGoal = Implemented(TraitRef)
| ProjectionEq(Projection = Type)
| Normalize(Projection -> Type)
| FromEnv(TraitRef)
| FromEnv(Projection = Type)
| WellFormed(Type)
| WellFormed(TraitRef)
| WellFormed(Projection = Type)
| Outlives(Type, Region)
| Outlives(Region, Region)
- `Implemented(TraitRef)` -- true if the given trait is
implemented for the given input types and lifetimes
- `FromEnv(TraitEnv)` -- true if the given trait is *assumed* to be implemented;
that is, if it can be derived from the in-scope where clauses
- 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].
- `ProjectionEq(Projection = Type)` -- the given associated type `Projection` is equal
to `Type`; see [the section on associated types](./traits-associated-types.html)
- `Normalize(Projection -> Type)` -- the given associated type `Projection` can be normalized
to `Type`
- as discussed in [the section on associated types](./traits-associated-types.html),
`Normalize` implies `ProjectionEq` but not vice versa
- `WellFormed(..)` -- these goals imply that the given item is
*well-formed*
- well-formedness is important to [implied bounds].
<a name=coinductive>
## Coinductive goals
Most goals in our system are "inductive". In an inductive goal,
circular reasoning is disallowed. Consider this example clause:
Implemented(Foo: Bar) :-
Implemented(Foo: Bar).
Considered inductively, this clause is useless: if we are trying to
prove `Implemented(Foo: Bar)`, we would then recursively have to prove
`Implemented(Foo: Bar)`, and that cycle would continue ad infinitum
(the trait solver will terminate here, it would just consider that
`Implemented(Foo: Bar)` is not known to be true).
However, some goals are *co-inductive*. Simply put, this means that
cycles are OK. So, if `Bar` were a co-inductive trait, then the rule
above would be perfectly valid, and it would indicate that
`Implemented(Foo: Bar)` is true.
*Auto traits* are one example in Rust where co-inductive goals are used.
Consider the `Send` trait, and imagine that we have this struct:
```rust
struct Foo {
next: Option<Box<Foo>>
}
```
The default rules for auto traits say that `Foo` is `Send` if the
types of its fields are `Send`. Therefore, we would have a rule like
Implemented(Foo: Send) :-
Implemented(Option<Box<Foo>>: Send).
As you can probably imagine, proving that `Option<Box<Foo>>: Send` is
going to wind up circularly requiring us to prove that `Foo: Send`
again. So this would be an example where we wind up in a cycle -- but
that's ok, we *do* consider `Foo: Send` to hold, even though it
references itself.
In general, co-inductive traits are used in Rust trait solving when we
want to enumerate a fixed set of possibilities. In the case of auto
traits, we are enumerating the set of reachable types from a given
starting point (i.e., `Foo` can reach values of type
`Option<Box<Foo>>`, which implies it can reach values of type
`Box<Foo>`, and then of type `Foo`, and then the cycle is complete).
In addition to auto traits, `WellFormed` predicates are co-inductive.
These are used to achieve a similar "enumerate all the cases" pattern,
as described in the section on [implied bounds].
[implied bounds]: ./traits-lowering-rules.html#implied-bounds
## Incomplete chapter
Some topics yet to be written:
- Elaborate on the proof procedure
- SLG solving -- introduce negative reasoning

267
src/traits-lowering-rules.md Normal file
View File

@ -0,0 +1,267 @@
# Lowering rules
This section gives the complete lowering rules for Rust traits into
[program clauses][pc]. These rules reference the [domain goals][dg] defined in
an earlier section.
[pc]: ./traits-goals-and-clauses.html
[dg]: ./traits-goals-and-clauses.html#domain-goals
## Notation
The nonterminal `Pi` is used to mean some generic *parameter*, either a
named lifetime like `'a` or a type paramter like `A`.
The nonterminal `Ai` is used to mean some generic *argument*, which
might be a lifetime like `'a` or a type like `Vec<A>`.
When defining the lowering rules, we will give goals and clauses in
the [notation given in this section](./traits-goals-and-clauses.html).
We sometimes insert "macros" like `LowerWhereClause!` into these
definitions; these macros reference other sections within this chapter.
## Lowering where clauses
When used in a goal position, where clauses can be mapped directly
[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)`
- `T: 'r` maps to `Outlives(T, 'r)`
- `'a: 'b` maps to `Outlives('a, 'b)`
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
where those where clauses appear as goals in the program clauses that
we are producing. In that case, the mapping above is used to convert
from the Rust syntax into goals.
### Transforming the lowered where clauses
In addition, in the rules below, we sometimes do some transformations
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)`
*TODO*: I suspect that we want to alter the outlives relations too,
but Chalk isn't modeling those right now.
## Lowering traits
Given a trait definition
```rust
trait Trait<P1..Pn> // P0 == Self
where WC
{
// trait items
}
```
we will produce a number of declarations. This section is focused on
the program clauses for the trait header (i.e., the stuff outside the
`{}`); the [section on trait items](#trait-items) covers the stuff
inside the `{}`.
### Trait header
From the trait itself we mostly make "meta" rules that setup the
relationships between different kinds of domain goals. The first dush
rule from the trait header creates the mapping between the `FromEnv`
and `Implemented` predicates:
forall<Self, P1..Pn> {
Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn)
}
<a name="implied-bounds">
#### 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]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html
// For each where clause WC:
forall<Self, P1..Pn> {
FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn)
}
This clause says that if we are assuming that the trait holds, then we can also
assume that it's where-clauses hold. It's perhaps useful to see an example:
```rust
trait Eq: PartialEq { ... }
```
In this case, the `PartialEq` supertrait is equivalent to a `where
Self: PartialEq` where clause, in our simplified model. The program
clause above therefore states that if we can prove `FromEnv(T: Eq)` --
e.g., if we are in some function with `T: Eq` in its where clauses --
then we also know that `FromEnv(T: PartialEq)`. Thus the set of things
that follow from the environment are not only the **direct where
clauses** but also things that follow from them.
The next rule is related; it defines what it means for a trait reference
to be **well-formed**:
// For each where clause WC:
forall<Self, P1..Pn> {
WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>), WellFormed(WC)
}
This `WellFormed` rule states that `T: Trait` is well-formed if (a)
`T: Trait` is implemented and (b) all the where-clauses declared on
`Trait` are well-formed (and hence they are implemented). Remember
that the `WellFormed` predicate is
[coinductive](./traits-goals-and-clauses.html#coinductive); in this
case, it is serving as a kind of "carrier" that allows us to enumerate
all the where clauses that are transitively implied by `T: Trait`.
An example:
```rust
trait Foo: A + Bar { }
trait Bar: B + Foo { }
trait A { }
trait B { }
```
Here, the transitive set of implications for `T: Foo` are `T: A`, `T: Bar`, and `T: B`.
And indeed if we were to try to prove `WellFormed(T: Foo)`, we would have to prove each
one of those:
- `WellFormed(T: Foo)`
- `Implemented(T: Foo)`
- `WellFormed(T: A)`
- `Implemented(T: A)`
- `WellFormed(T: Bar)`
- `Implemented(T: Bar)`
- `WellFormed(T: B)`
- `Implemented(T: Bar)`
- `WellFormed(T: Foo)` -- cycle, true coinductively
This `WellFormed` predicate is only used when proving that impls are
well-formed -- basically, for each impl of some trait ref `TraitRef`,
we must that `WellFormed(TraitRef)`. This in turn justifies the
implied bounds rules that allow us to extend the set of `FromEnv`
items.
<a name=trait-items>
## Lowering trait items
### Associated type declarations
Given a trait that declares a (possibly generic) associated type:
```rust
trait Trait<P1..Pn> // P0 == Self
where WC
{
type AssocType<Pn+1..Pm>: Bounds where WC1;
}
```
We will produce a number of program clases. The first two define
the rules by which `ProjectionEq` can succeed; these two clauses are discussed
in detail in the [section on associated types](./traits-associated-types.html).
// ProjectionEq can succeed by normalizing:
forall<Self, P1..Pn, Pn+1..Pm, U> {
ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U) :-
Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U)
}
// ProjectionEq can succeed by skolemizing:
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>
) :-
// But only if the trait is implemented, and the conditions from
// the associated type are met as well:
Implemented(Self: Trait<P1..Pn>),
WC1
}
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
elsewhere.
// XXX how exactly should we set this up? Have to be careful;
// presumably this has to be a kind of `FromEnv` setup.
### Lowering function and constant declarations
Chalk didn't model functions and constants, but I would eventually
like to treat them exactly like normalization. See [the section on function/constant
values below](#constant-vals) for more details.
## Lowering impls
Given an impl of a trait:
```rust
impl<P0..Pn> Trait<A1..An> for A0
where WC
{
// zero or more impl items
}
```
Let `TraitRef` be the trait reference `A0: Trait<A1..An>`. Then we
will create the following rules:
forall<P0..Pn> {
Implemented(TraitRef) :- WC
}
In addition, we will lower all of the *impl items*.
## Lowering impl items
### Associated type values
Given an impl that contains:
```rust
impl<P0..Pn> Trait<A1..An> for A0
where WC
{
type AssocType<Pn+1..Pm>: Bounds where WC1 = T;
}
```
We produce the following rule:
forall<P0..Pm> {
forall<Pn+1..Pm> {
Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
WC, WC1
}
}
Note that `WC` and `WC1` both encode where-clauses that the impl can
rely on, whereas the bounds `Bounds` on the associated type are things
that the impl must prove (see the well-formedness checking).
<a name=constant-vals>
### Function and constant values
Chalk didn't model functions and constants, but I would eventually
like to treat them exactly like normalization. This presumably
involves adding a new kind of parameter (constant), and then having a
`NormalizeValue` domain goal. This is *to be written* because the
details are a bit up in the air.

182
src/traits-lowering-to-logic.md Normal file
View File

@ -0,0 +1,182 @@
# Lowering to logic
The key observation here is that the Rust trait system is basically a
kind of logic, and it can be mapped onto standard logical inference
rules. We can then look for solutions to those inference rules in a
very similar fashion to how e.g. a [Prolog] solver works. It turns out
that we can't *quite* use Prolog rules (also called Horn clauses) but
rather need a somewhat more expressive variant.
[Prolog]: https://en.wikipedia.org/wiki/Prolog
## Rust traits and logic
One of the first observations is that the Rust trait system is
basically a kind of logic. As such, we can map our struct, trait, and
impl declarations into logical inference rules. For the most part,
these are basically Horn clauses, though we'll see that to capture the
full richness of Rust -- and in particular to support generic
programming -- we have to go a bit further than standard Horn clauses.
To see how this mapping works, let's start with an example. Imagine
we declare a trait and a few impls, like so:
```rust
trait Clone { }
impl Clone for usize { }
impl<T> Clone for Vec<T> where T: Clone { }
```
We could map these declarations to some Horn clauses, written in a
Prolog-like notation, as follows:
```
Clone(usize).
Clone(Vec<?T>) :- Clone(?T).
```
In Prolog terms, we might say that `Clone(Foo)` -- where `Foo` is some
Rust type -- is a *predicate* that represents the idea that the type
`Foo` implements `Clone`. These rules are **program clauses**; they
state the conditions under which that predicate can be proven (i.e.,
considered true). So the first rule just says "Clone is implemented
for `usize`". The next rule says "for any type `?T`, Clone is
implemented for `Vec<?T>` if clone is implemented for `?T`". So
e.g. if we wanted to prove that `Clone(Vec<Vec<usize>>)`, we would do
so by applying the rules recursively:
- `Clone(Vec<Vec<usize>>)` is provable if:
- `Clone(Vec<usize>)` is provable if:
- `Clone(usize)` is provable. (Which is is, so we're all good.)
But now suppose we tried to prove that `Clone(Vec<Bar>)`. This would
fail (after all, I didn't give an impl of `Clone` for `Bar`):
- `Clone(Vec<Bar>)` is provable if:
- `Clone(Bar)` is provable. (But it is not, as there are no applicable rules.)
We can easily extend the example above to cover generic traits with
more than one input type. So imagine the `Eq<T>` trait, which declares
that `Self` is equatable with a value of type `T`:
```rust
trait Eq<T> { ... }
impl Eq<usize> for usize { }
impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }
```
That could be mapped as follows:
```
Eq(usize, usize).
Eq(Vec<?T>, Vec<?U>) :- Eq(?T, ?U).
```
So far so good.
## Type-checking normal functions
OK, now that we have defined some logical rules that are able to
express when traits are implemented and to handle associated types,
let's turn our focus a bit towards **type-checking**. Type-checking is
interesting because it is what gives us the goals that we need to
prove. That is, everything we've seen so far has been about how we
derive the rules by which we can prove goals from the traits and impls
in the program; but we are also interesting in how derive the goals
that we need to prove, and those come from type-checking.
Consider type-checking the function `foo()` here:
```rust
fn foo() { bar::<usize>() }
fn bar<U: Eq>() { }
```
This function is very simple, of course: all it does is to call
`bar::<usize>()`. Now, looking at the definition of `bar()`, we can see
that it has one where-clause `U: Eq`. So, that means that `foo()` will
have to prove that `usize: Eq` in order to show that it can call `bar()`
with `usize` as the type argument.
If we wanted, we could write a Prolog predicate that defines the
conditions under which `bar()` can be called. We'll say that those
conditions are called being "well-formed":
```
barWellFormed(?U) :- Eq(?U).
```
Then we can say that `foo()` type-checks if the reference to
`bar::<usize>` (that is, `bar()` applied to the type `usize`) is
well-formed:
```
fooTypeChecks :- barWellFormed(usize).
```
If we try to prove the goal `fooTypeChecks`, it will succeed:
- `fooTypeChecks` is provable if:
- `barWellFormed(usize)`, which is provable if:
- `Eq(usize)`, which is provable because of an impl.
Ok, so far so good. Let's move on to type-checking a more complex function.
## Type-checking generic functions: beyond Horn clauses
In the last section, we used standard Prolog horn-clauses (augmented with Rust's
notion of type equality) to type-check some simple Rust functions. But that only
works when we are type-checking non-generic functions. If we want to type-check
a generic function, it turns out we need a stronger notion of goal than Prolog
can be provide. To see what I'm talking about, let's revamp our previous
example to make `foo` generic:
```rust
fn foo<T: Eq>() { bar::<T>() }
fn bar<U: Eq>() { }
```
To type-check the body of `foo`, we need to be able to hold the type
`T` "abstract". That is, we need to check that the body of `foo` is
type-safe *for all types `T`*, not just for some specific type. We might express
this like so:
```
fooTypeChecks :-
// for all types T...
forall<T> {
// ...if we assume that Eq(T) is provable...
if (Eq(T)) {
// ...then we can prove that `barWellFormed(T)` holds.
barWellFormed(T)
}
}.
```
This notation I'm using here is the notation I've been using in my
prototype implementation; it's similar to standard mathematical
notation but a bit Rustified. Anyway, the problem is that standard
Horn clauses don't allow universal quantification (`forall`) or
implication (`if`) in goals (though many Prolog engines do support
them, as an extension). For this reason, we need to accept something
called "first-order hereditary harrop" (FOHH) clauses -- this long
name basically means "standard Horn clauses with `forall` and `if` in
the body". But it's nice to know the proper name, because there is a
lot of work describing how to efficiently handle FOHH clauses; see for
example Gopalan Nadathur's excellent
["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
in [the bibliography].
[the bibliography]: ./traits-bibliography.html
[pphhf]: ./traits-bibliography.html#pphhf
It turns out that supporting FOHH is not really all that hard. And
once we are able to do that, we can easily describe the type-checking
rule for generic functions like `foo` in our logic.
## Source
This page is a lightly adapted version of a
[blog post by Nicholas Matsakis][lrtl].
[lrtl]: http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/

3
src/traits-regions.md Normal file
View File

@ -0,0 +1,3 @@
# Region constraints
*to be written*

11
src/traits-wf.md Normal file
View File

@ -0,0 +1,11 @@
# Well-formedness checking
This chapter is mostly *to be written*. WF checking, in short, has the
job of checking that the various declarations in a Rust program are
well-formed. This is the basis for implied bounds, and partly for that
reason, this checking can be surprisingly subtle! (For example, we
have to be sure that each impl proves the WF conditions declared on
the trait.)

18
src/traits.md Normal file
View File

@ -0,0 +1,18 @@
# Trait solving (new-style)
🚧 This chapter describes "new-style" trait solving. This is still in
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).🚧
Trait solving is based around a few key ideas:
- [Canonicalization](./traits-canonicalization.html), which allows us to
extract types that contain inference variables in them from their
inference context, work with them, and then bring the results back
into the original context.
- [Lowering to logic](./traits-lowering-to-logic.html), which expresses
Rust traits in terms of standard logical terms.
*more to come*

2
src/type-inference.md
View File

@ -43,6 +43,8 @@ The `tcx.infer_ctxt` method actually returns a builder, which means
there are some kinds of configuration you can do before the `infcx` is
created. See `InferCtxtBuilder` for more information.
<a name=vars>
## Inference variables
The main purpose of the inference context is to house a bunch of