From 479d914ff009a0372427b42f3796f5937297644f Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Tue, 27 Feb 2018 05:50:43 -0500 Subject: [PATCH] work on traits chapters --- src/SUMMARY.md | 13 +- src/trait-resolution.md | 7 +- src/traits-associated-types.md | 143 +++++++++++++++++ src/traits-bibliography.md | 28 ++++ src/traits-canonicalization.md | 93 +++++++++++ src/traits-goals-and-clauses.md | 148 ++++++++++++++++++ src/traits-lowering-rules.md | 267 ++++++++++++++++++++++++++++++++ src/traits-lowering-to-logic.md | 182 ++++++++++++++++++++++ src/traits-regions.md | 3 + src/traits-wf.md | 11 ++ src/traits.md | 18 +++ src/type-inference.md | 2 + 12 files changed, 912 insertions(+), 3 deletions(-) create mode 100644 src/traits-associated-types.md create mode 100644 src/traits-bibliography.md create mode 100644 src/traits-canonicalization.md create mode 100644 src/traits-goals-and-clauses.md create mode 100644 src/traits-lowering-rules.md create mode 100644 src/traits-lowering-to-logic.md create mode 100644 src/traits-regions.md create mode 100644 src/traits-wf.md create mode 100644 src/traits.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index ab9da729..1c5bc284 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -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) diff --git a/src/trait-resolution.md b/src/trait-resolution.md index 28176d74..cccfcd54 100644 --- a/src/trait-resolution.md +++ b/src/trait-resolution.md @@ -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 diff --git a/src/traits-associated-types.md b/src/traits-associated-types.md new file mode 100644 index 00000000..a640bf03 --- /dev/null +++ b/src/traits-associated-types.md @@ -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 ` 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` +declares (among other things) that `Item = T`: + +```rust +impl IntoIterator for Option { + type Item = T; + .. +} +``` + +This means we can normalize the projection ` 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, +` 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` that +we saw above would be lowered to a program clause like so: + + forall { + Normalize( 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(...) { ... } +``` + +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)`. 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 +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. +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(::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 { + ProjectionEq(::Item = U) :- + Normalize(::Item -> U) + } + + forall { + ProjectionEq(::Item = (IntoIterator::Item)) + } + +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) + diff --git a/src/traits-bibliography.md b/src/traits-bibliography.md new file mode 100644 index 00000000..d9ff912c --- /dev/null +++ b/src/traits-bibliography.md @@ -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 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 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/ diff --git a/src/traits-canonicalization.md b/src/traits-canonicalization.md new file mode 100644 index 00000000..35352d60 --- /dev/null +++ b/src/traits-canonicalization.md @@ -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 { ?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, '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, '?X, ?C ] + ^^ ^^^ fresh inference variables in `self` + .. +} +``` + +Step (b) would then unify: + +``` +?A with Vec +'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.) + diff --git a/src/traits-goals-and-clauses.md b/src/traits-goals-and-clauses.md new file mode 100644 index 00000000..ad165572 --- /dev/null +++ b/src/traits-goals-and-clauses.md @@ -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 { Goal } // existential quantification + | forall { Goal } // universal quantification + | if (Clause) { Goal } // implication + + Clause = DomainGoal + | Clause :- Goal // if can prove Goal, then Clause is true + | Clause && Clause + | forall { Clause } + + K = // a "kind" + | + +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 + + + +## 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 + +So, for example, `u32: Display` is a trait reference, as is `Vec: +IntoIterator`. Note that Rust surface syntax also permits some extra +things, like associated type bindings (`Vec: IntoIterator`), that are not part of a trait reference. + +A **projection** consists of a an associated item reference along with +its inputs P0..Pm: + + Projection = >::AssocItem + +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]. + + + +## 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> +} +``` + +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>: Send). + +As you can probably imagine, proving that `Option>: 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>`, which implies it can reach values of type +`Box`, 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 diff --git a/src/traits-lowering-rules.md b/src/traits-lowering-rules.md new file mode 100644 index 00000000..d096b436 --- /dev/null +++ b/src/traits-lowering-rules.md @@ -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`. + +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` maps to `Implemented(A0: Foo)`. +- `A0: Foo` maps to `ProjectionEq(>::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 // 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 { + Implemented(Self: Trait) :- FromEnv(Self: Trait + +#### 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 { + FromEnv(WC) :- FromEnv(Self: Trait { + WellFormed(Self: Trait) :- Implemented(Self: Trait), 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. + + + +## Lowering trait items + +### Associated type declarations + +Given a trait that declares a (possibly generic) associated type: + +```rust +trait Trait // P0 == Self +where WC +{ + type AssocType: 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 { + ProjectionEq(>::AssocType = U) :- + Normalize(>::AssocType -> U) + } + + // ProjectionEq can succeed by skolemizing: + forall { + ProjectionEq( + >::AssocType = + (Trait::AssocType) + ) :- + // But only if the trait is implemented, and the conditions from + // the associated type are met as well: + Implemented(Self: Trait), + 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 Trait for A0 +where WC +{ + // zero or more impl items +} +``` + +Let `TraitRef` be the trait reference `A0: Trait`. Then we +will create the following rules: + + forall { + 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 Trait for A0 +where WC +{ + type AssocType: Bounds where WC1 = T; +} +``` + +We produce the following rule: + + forall { + forall { + Normalize(>::AssocType -> 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). + + + +### 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. + + diff --git a/src/traits-lowering-to-logic.md b/src/traits-lowering-to-logic.md new file mode 100644 index 00000000..7b1c2ed6 --- /dev/null +++ b/src/traits-lowering-to-logic.md @@ -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 Clone for Vec where T: Clone { } +``` + +We could map these declarations to some Horn clauses, written in a +Prolog-like notation, as follows: + +``` +Clone(usize). +Clone(Vec) :- 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` if clone is implemented for `?T`". So +e.g. if we wanted to prove that `Clone(Vec>)`, we would do +so by applying the rules recursively: + +- `Clone(Vec>)` is provable if: + - `Clone(Vec)` 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)`. This would +fail (after all, I didn't give an impl of `Clone` for `Bar`): + +- `Clone(Vec)` 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` trait, which declares +that `Self` is equatable with a value of type `T`: + +```rust +trait Eq { ... } +impl Eq for usize { } +impl> Eq> for Vec { } +``` + +That could be mapped as follows: + +``` +Eq(usize, usize). +Eq(Vec, Vec) :- 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::() } +fn bar() { } +``` + +This function is very simple, of course: all it does is to call +`bar::()`. 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::` (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() { bar::() } +fn bar() { } +``` + +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 { + // ...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/ diff --git a/src/traits-regions.md b/src/traits-regions.md new file mode 100644 index 00000000..baa3582b --- /dev/null +++ b/src/traits-regions.md @@ -0,0 +1,3 @@ +# Region constraints + +*to be written* diff --git a/src/traits-wf.md b/src/traits-wf.md new file mode 100644 index 00000000..c002b8cc --- /dev/null +++ b/src/traits-wf.md @@ -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.) + + + diff --git a/src/traits.md b/src/traits.md new file mode 100644 index 00000000..28e27e82 --- /dev/null +++ b/src/traits.md @@ -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* diff --git a/src/type-inference.md b/src/type-inference.md index 8812d34d..3795ea70 100644 --- a/src/type-inference.md +++ b/src/type-inference.md @@ -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. + + ## Inference variables The main purpose of the inference context is to house a bunch of