1+ /*!
2+
3+ # Type inference engine
4+
5+ This is loosely based on standard HM-type inference, but with an
6+ extension to try and accommodate subtyping. There is nothing
7+ principled about this extension; it's sound---I hope!---but it's a
8+ heuristic, ultimately, and does not guarantee that it finds a valid
9+ typing even if one exists (in fact, there are known scenarios where it
10+ fails, some of which may eventually become problematic).
11+
12+ ## Key idea
13+
14+ The main change is that each type variable T is associated with a
15+ lower-bound L and an upper-bound U. L and U begin as bottom and top,
16+ respectively, but gradually narrow in response to new constraints
17+ being introduced. When a variable is finally resolved to a concrete
18+ type, it can (theoretically) select any type that is a supertype of L
19+ and a subtype of U.
20+
21+ There are several critical invariants which we maintain:
22+
23+ - the upper-bound of a variable only becomes lower and the lower-bound
24+ only becomes higher over time;
25+ - the lower-bound L is always a subtype of the upper bound U;
26+ - the lower-bound L and upper-bound U never refer to other type variables,
27+ but only to types (though those types may contain type variables).
28+
29+ > An aside: if the terms upper- and lower-bound confuse you, think of
30+ > "supertype" and "subtype". The upper-bound is a "supertype"
31+ > (super=upper in Latin, or something like that anyway) and the lower-bound
32+ > is a "subtype" (sub=lower in Latin). I find it helps to visualize
33+ > a simple class hierarchy, like Java minus interfaces and
34+ > primitive types. The class Object is at the root (top) and other
35+ > types lie in between. The bottom type is then the Null type.
36+ > So the tree looks like:
37+ >
38+ > Object
39+ > / \
40+ > String Other
41+ > \ /
42+ > (null)
43+ >
44+ > So the upper bound type is the "supertype" and the lower bound is the
45+ > "subtype" (also, super and sub mean upper and lower in Latin, or something
46+ > like that anyway).
47+
48+ ## Satisfying constraints
49+
50+ At a primitive level, there is only one form of constraint that the
51+ inference understands: a subtype relation. So the outside world can
52+ say "make type A a subtype of type B". If there are variables
53+ involved, the inferencer will adjust their upper- and lower-bounds as
54+ needed to ensure that this relation is satisfied. (We also allow "make
55+ type A equal to type B", but this is translated into "A <: B" and "B
56+ <: A")
57+
58+ As stated above, we always maintain the invariant that type bounds
59+ never refer to other variables. This keeps the inference relatively
60+ simple, avoiding the scenario of having a kind of graph where we have
61+ to pump constraints along and reach a fixed point, but it does impose
62+ some heuristics in the case where the user is relating two type
63+ variables A <: B.
64+
65+ Combining two variables such that variable A will forever be a subtype
66+ of variable B is the trickiest part of the algorithm because there is
67+ often no right choice---that is, the right choice will depend on
68+ future constraints which we do not yet know. The problem comes about
69+ because both A and B have bounds that can be adjusted in the future.
70+ Let's look at some of the cases that can come up.
71+
72+ Imagine, to start, the best case, where both A and B have an upper and
73+ lower bound (that is, the bounds are not top nor bot respectively). In
74+ that case, if we're lucky, A.ub <: B.lb, and so we know that whatever
75+ A and B should become, they will forever have the desired subtyping
76+ relation. We can just leave things as they are.
77+
78+ ### Option 1: Unify
79+
80+ However, suppose that A.ub is *not* a subtype of B.lb. In
81+ that case, we must make a decision. One option is to unify A
82+ and B so that they are one variable whose bounds are:
83+
84+ UB = GLB(A.ub, B.ub)
85+ LB = LUB(A.lb, B.lb)
86+
87+ (Note that we will have to verify that LB <: UB; if it does not, the
88+ types are not intersecting and there is an error) In that case, A <: B
89+ holds trivially because A==B. However, we have now lost some
90+ flexibility, because perhaps the user intended for A and B to end up
91+ as different types and not the same type.
92+
93+ Pictorally, what this does is to take two distinct variables with
94+ (hopefully not completely) distinct type ranges and produce one with
95+ the intersection.
96+
97+ B.ub B.ub
98+ /\ /
99+ A.ub / \ A.ub /
100+ / \ / \ \ /
101+ / X \ UB
102+ / / \ \ / \
103+ / / / \ / /
104+ \ \ / / \ /
105+ \ X / LB
106+ \ / \ / / \
107+ \ / \ / / \
108+ A.lb B.lb A.lb B.lb
109+
110+
111+ ### Option 2: Relate UB/LB
112+
113+ Another option is to keep A and B as distinct variables but set their
114+ bounds in such a way that, whatever happens, we know that A <: B will hold.
115+ This can be achieved by ensuring that A.ub <: B.lb. In practice there
116+ are two ways to do that, depicted pictorally here:
117+
118+ Before Option #1 Option #2
119+
120+ B.ub B.ub B.ub
121+ /\ / \ / \
122+ A.ub / \ A.ub /(B')\ A.ub /(B')\
123+ / \ / \ \ / / \ / /
124+ / X \ __UB____/ UB /
125+ / / \ \ / | | /
126+ / / / \ / | | /
127+ \ \ / / /(A')| | /
128+ \ X / / LB ______LB/
129+ \ / \ / / / \ / (A')/ \
130+ \ / \ / \ / \ \ / \
131+ A.lb B.lb A.lb B.lb A.lb B.lb
132+
133+ In these diagrams, UB and LB are defined as before. As you can see,
134+ the new ranges `A'` and `B'` are quite different from the range that
135+ would be produced by unifying the variables.
136+
137+ ### What we do now
138+
139+ Our current technique is to *try* (transactionally) to relate the
140+ existing bounds of A and B, if there are any (i.e., if `UB(A) != top
141+ && LB(B) != bot`). If that succeeds, we're done. If it fails, then
142+ we merge A and B into same variable.
143+
144+ This is not clearly the correct course. For example, if `UB(A) !=
145+ top` but `LB(B) == bot`, we could conceivably set `LB(B)` to `UB(A)`
146+ and leave the variables unmerged. This is sometimes the better
147+ course, it depends on the program.
148+
149+ The main case which fails today that I would like to support is:
150+
151+ fn foo<T>(x: T, y: T) { ... }
152+
153+ fn bar() {
154+ let x: @mut int = @mut 3;
155+ let y: @int = @3;
156+ foo(x, y);
157+ }
158+
159+ In principle, the inferencer ought to find that the parameter `T` to
160+ `foo(x, y)` is `@const int`. Today, however, it does not; this is
161+ because the type variable `T` is merged with the type variable for
162+ `X`, and thus inherits its UB/LB of `@mut int`. This leaves no
163+ flexibility for `T` to later adjust to accommodate `@int`.
164+
165+ ### What to do when not all bounds are present
166+
167+ In the prior discussion we assumed that A.ub was not top and B.lb was
168+ not bot. Unfortunately this is rarely the case. Often type variables
169+ have "lopsided" bounds. For example, if a variable in the program has
170+ been initialized but has not been used, then its corresponding type
171+ variable will have a lower bound but no upper bound. When that
172+ variable is then used, we would like to know its upper bound---but we
173+ don't have one! In this case we'll do different things depending on
174+ how the variable is being used.
175+
176+ ## Transactional support
177+
178+ Whenever we adjust merge variables or adjust their bounds, we always
179+ keep a record of the old value. This allows the changes to be undone.
180+
181+ ## Regions
182+
183+ I've only talked about type variables here, but region variables
184+ follow the same principle. They have upper- and lower-bounds. A
185+ region A is a subregion of a region B if A being valid implies that B
186+ is valid. This basically corresponds to the block nesting structure:
187+ the regions for outer block scopes are superregions of those for inner
188+ block scopes.
189+
190+ ## Integral and floating-point type variables
191+
192+ There is a third variety of type variable that we use only for
193+ inferring the types of unsuffixed integer literals. Integral type
194+ variables differ from general-purpose type variables in that there's
195+ no subtyping relationship among the various integral types, so instead
196+ of associating each variable with an upper and lower bound, we just
197+ use simple unification. Each integer variable is associated with at
198+ most one integer type. Floating point types are handled similarly to
199+ integral types.
200+
201+ ## GLB/LUB
202+
203+ Computing the greatest-lower-bound and least-upper-bound of two
204+ types/regions is generally straightforward except when type variables
205+ are involved. In that case, we follow a similar "try to use the bounds
206+ when possible but otherwise merge the variables" strategy. In other
207+ words, `GLB(A, B)` where `A` and `B` are variables will often result
208+ in `A` and `B` being merged and the result being `A`.
209+
210+ ## Type coercion
211+
212+ We have a notion of assignability which differs somewhat from
213+ subtyping; in particular it may cause region borrowing to occur. See
214+ the big comment later in this file on Type Coercion for specifics.
215+
216+ ### In conclusion
217+
218+ I showed you three ways to relate `A` and `B`. There are also more,
219+ of course, though I'm not sure if there are any more sensible options.
220+ The main point is that there are various options, each of which
221+ produce a distinct range of types for `A` and `B`. Depending on what
222+ the correct values for A and B are, one of these options will be the
223+ right choice: but of course we don't know the right values for A and B
224+ yet, that's what we're trying to find! In our code, we opt to unify
225+ (Option #1).
226+
227+ # Implementation details
228+
229+ We make use of a trait-like impementation strategy to consolidate
230+ duplicated code between subtypes, GLB, and LUB computations. See the
231+ section on "Type Combining" below for details.
232+
233+ */
0 commit comments