Merge pull request #70 from nikomatsakis/traits

work on traits chapters

Author: nikomatsakis

src/SUMMARY.md

@@ -17,10 +17,22 @@
 - [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)
+    - [Lowering to logic](./traits-lowering-to-logic.md)
+      - [Goals and clauses](./traits-goals-and-clauses.md)
+      - [Equality and associated types](./traits-associated-types.md)
+      - [Implied bounds](./traits-implied-bounds.md)
+      - [Region constraints](./traits-regions.md)
+    - [Canonical queries](./traits-canonical-queries.md)
+      - [Canonicalization](./traits-canonicalization.md)
+    - [Lowering rules](./traits-lowering-rules.md)
+    - [Well-formedness checking](./traits-wf.md)
+    - [The SLG solver](./traits-slg.md)
+    - [Bibliography](./traits-bibliography.md)
 - [Type checking](./type-checking.md)
 - [The MIR (Mid-level IR)](./mir.md)
     - [MIR construction](./mir-construction.md)

src/glossary.md

@@ -31,10 +31,12 @@ LTO                     |  Link-Time Optimizations. A set of optimizations offer
 [LLVM]                  |  (actually not an acronym :P) an open-source compiler backend. It accepts LLVM IR and outputs native binaries. Various languages (e.g. Rust) can then implement a compiler front-end that output LLVM IR and use LLVM to compile to all the platforms LLVM supports.
 MIR                     |  the Mid-level IR that is created after type-checking for use by borrowck and trans ([see more](./mir.html))
 miri                    |  an interpreter for MIR used for constant evaluation ([see more](./miri.html))
+normalize               |  a general term for converting to a more canonical form, but in the case of rustc typically refers to [associated type normalization](./traits-associated-types.html#normalize)
 newtype                 |  a "newtype" is a wrapper around some other type (e.g., `struct Foo(T)` is a "newtype" for `T`). This is commonly used in Rust to give a stronger type for indices.
 NLL                     | [non-lexical lifetimes](./mir-regionck.html), an extension to Rust's borrowing system to make it be based on the control-flow graph.
 node-id or NodeId       |  an index identifying a particular node in the AST or HIR; gradually being phased out and replaced with `HirId`.
 obligation              |  something that must be proven by the trait system ([see more](trait-resolution.html))
+projection              |  a general term for a "relative path", e.g. `x.f` is a "field projection", and `T::Item` is an ["associated type projection"](./traits-goals-and-clauses.html#trait-ref)
 promoted constants      |  constants extracted from a function and lifted to static scope; see [this section](./mir.html#promoted) for more details.
 provider                |  the function that executes a query ([see more](query.html))
 quantified              |  in math or logic, existential and universal quantification are used to ask questions like "is there any type T for which is true?" or "is this true for all types T?"; see [the background chapter for more](./background.html#quantified)  
@@ -49,6 +51,7 @@ span                    |  a location in the user's source code, used for error
 substs                  |  the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap<i32, u32>`)
 tcx                     |  the "typing context", main data structure of the compiler ([see more](ty.html))
 'tcx                    |  the lifetime of the currently active inference context ([see more](ty.html))
+trait reference         |  the name of a trait along with a suitable set of input type/lifetimes ([see more](./traits-goals-and-clauses.html#trait-ref))
 token                   |  the smallest unit of parsing. Tokens are produced after lexing ([see more](the-parser.html)).
 [TLS]                   |  Thread-Local Storage. Variables may be defined so that each thread has its own copy (rather than all threads sharing the variable). This has some interactions with LLVM. Not all platforms support TLS.
 trans                   |  the code to translate MIR into LLVM IR.

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 [*this* traits chapter](./traits.html).
+
 ## Major concepts
 
 Trait resolution is the process of pairing up an impl with each

src/traits-associated-types.md

@@ -0,0 +1,145 @@
+# 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.)
+
+<a name=normalize>
+
+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)
+

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 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/