Skip to content
Prev Previous commit
Next Next commit
don't say 'thing'
  • Loading branch information
nikomatsakis committed Mar 10, 2018
commit fd92491375f30b89050ebe51130112d1cee8896e
16 changes: 9 additions & 7 deletions src/traits-canonicalization.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,15 @@

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).
[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 data-structure T that contains types/regions from its
environment, we just walk down and find the unbound variables that
appear in T; those variables get replaced with "canonical variables",
starting from zero and numbered in a fixed 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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You may want to introduce the existential ? before this?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

hmm. I sort of do, by saying "where ?T are inference variables", but it does feel like there is some missing introductory material. And maybe a notation section. I have to mull on this.

`?U` are distinct, unbound inference variables, then the canonical
Expand Down