Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

work on traits chapters #70

Merged
merged 13 commits into from
Mar 10, 2018
16 changes: 14 additions & 2 deletions src/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
3 changes: 3 additions & 0 deletions src/glossary.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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.
Expand Down
7 changes: 6 additions & 1 deletion src/trait-resolution.md
Original file line number Diff line number Diff line change
@@ -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
Expand Down
145 changes: 145 additions & 0 deletions src/traits-associated-types.md
Original file line number Diff line number Diff line change
@@ -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)

28 changes: 28 additions & 0 deletions src/traits-bibliography.md
Original file line number Diff line number Diff line change
@@ -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/