1 // Copyright 2012 The Rust Project Developers. See the COPYRIGHT
2 // file at the top-level directory of this distribution and at
3 // http://rust-lang.org/COPYRIGHT.
4 //
5 // Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
6 // http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
7 // <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
8 // option. This file may not be copied, modified, or distributed
9 // except according to those terms.
10
11 /*!
12
13 Region inference module.
14
15 # Terminology
16
17 Note that we use the terms region and lifetime interchangeably,
18 though the term `lifetime` is preferred.
19
20 # Introduction
21
22 Region inference uses a somewhat more involved algorithm than type
23 inference. It is not the most efficient thing ever written though it
24 seems to work well enough in practice (famous last words). The reason
25 that we use a different algorithm is because, unlike with types, it is
26 impractical to hand-annotate with regions (in some cases, there aren't
27 even the requisite syntactic forms). So we have to get it right, and
28 it's worth spending more time on a more involved analysis. Moreover,
29 regions are a simpler case than types: they don't have aggregate
30 structure, for example.
31
32 Unlike normal type inference, which is similar in spirit to H-M and thus
33 works progressively, the region type inference works by accumulating
34 constraints over the course of a function. Finally, at the end of
35 processing a function, we process and solve the constraints all at
36 once.
37
38 The constraints are always of one of three possible forms:
39
40 - ConstrainVarSubVar(R_i, R_j) states that region variable R_i
41 must be a subregion of R_j
42 - ConstrainRegSubVar(R, R_i) states that the concrete region R
43 (which must not be a variable) must be a subregion of the varibale R_i
44 - ConstrainVarSubReg(R_i, R) is the inverse
45
46 # Building up the constraints
47
48 Variables and constraints are created using the following methods:
49
50 - `new_region_var()` creates a new, unconstrained region variable;
51 - `make_subregion(R_i, R_j)` states that R_i is a subregion of R_j
52 - `lub_regions(R_i, R_j) -> R_k` returns a region R_k which is
53 the smallest region that is greater than both R_i and R_j
54 - `glb_regions(R_i, R_j) -> R_k` returns a region R_k which is
55 the greatest region that is smaller than both R_i and R_j
56
57 The actual region resolution algorithm is not entirely
58 obvious, though it is also not overly complex.
59
60 ## Snapshotting
61
62 It is also permitted to try (and rollback) changes to the graph. This
63 is done by invoking `start_snapshot()`, which returns a value. Then
64 later you can call `rollback_to()` which undoes the work.
65 Alternatively, you can call `commit()` which ends all snapshots.
66 Snapshots can be recursive---so you can start a snapshot when another
67 is in progress, but only the root snapshot can "commit".
68
69 # Resolving constraints
70
71 The constraint resolution algorithm is not super complex but also not
72 entirely obvious. Here I describe the problem somewhat abstractly,
73 then describe how the current code works. There may be other, smarter
74 ways of doing this with which I am unfamiliar and can't be bothered to
75 research at the moment. - NDM
76
77 ## The problem
78
79 Basically our input is a directed graph where nodes can be divided
80 into two categories: region variables and concrete regions. Each edge
81 `R -> S` in the graph represents a constraint that the region `R` is a
82 subregion of the region `S`.
83
84 Region variable nodes can have arbitrary degree. There is one region
85 variable node per region variable.
86
87 Each concrete region node is associated with some, well, concrete
88 region: e.g., a free lifetime, or the region for a particular scope.
89 Note that there may be more than one concrete region node for a
90 particular region value. Moreover, because of how the graph is built,
91 we know that all concrete region nodes have either in-degree 1 or
92 out-degree 1.
93
94 Before resolution begins, we build up the constraints in a hashmap
95 that maps `Constraint` keys to spans. During resolution, we construct
96 the actual `Graph` structure that we describe here.
97
98 ## Our current algorithm
99
100 We divide region variables into two groups: Expanding and Contracting.
101 Expanding region variables are those that have a concrete region
102 predecessor (direct or indirect). Contracting region variables are
103 all others.
104
105 We first resolve the values of Expanding region variables and then
106 process Contracting ones. We currently use an iterative, fixed-point
107 procedure (but read on, I believe this could be replaced with a linear
108 walk). Basically we iterate over the edges in the graph, ensuring
109 that, if the source of the edge has a value, then this value is a
110 subregion of the target value. If the target does not yet have a
111 value, it takes the value from the source. If the target already had
112 a value, then the resulting value is Least Upper Bound of the old and
113 new values. When we are done, each Expanding node will have the
114 smallest region that it could possibly have and still satisfy the
115 constraints.
116
117 We next process the Contracting nodes. Here we again iterate over the
118 edges, only this time we move values from target to source (if the
119 source is a Contracting node). For each contracting node, we compute
120 its value as the GLB of all its successors. Basically contracting
121 nodes ensure that there is overlap between their successors; we will
122 ultimately infer the largest overlap possible.
123
124 # The Region Hierarchy
125
126 ## Without closures
127
128 Let's first consider the region hierarchy without thinking about
129 closures, because they add a lot of complications. The region
130 hierarchy *basically* mirrors the lexical structure of the code.
131 There is a region for every piece of 'evaluation' that occurs, meaning
132 every expression, block, and pattern (patterns are considered to
133 "execute" by testing the value they are applied to and creating any
134 relevant bindings). So, for example:
135
136 fn foo(x: int, y: int) { // -+
137 // +------------+ // |
138 // | +-----+ // |
139 // | +-+ +-+ +-+ // |
140 // | | | | | | | // |
141 // v v v v v v v // |
142 let z = x + y; // |
143 ... // |
144 } // -+
145
146 fn bar() { ... }
147
148 In this example, there is a region for the fn body block as a whole,
149 and then a subregion for the declaration of the local variable.
150 Within that, there are sublifetimes for the assignment pattern and
151 also the expression `x + y`. The expression itself has sublifetimes
152 for evaluating `x` and `y`.
153
154 ## Function calls
155
156 Function calls are a bit tricky. I will describe how we handle them
157 *now* and then a bit about how we can improve them (Issue #6268).
158
159 Consider a function call like `func(expr1, expr2)`, where `func`,
160 `arg1`, and `arg2` are all arbitrary expressions. Currently,
161 we construct a region hierarchy like:
162
163 +----------------+
164 | |
165 +--+ +---+ +---+|
166 v v v v v vv
167 func(expr1, expr2)
168
169 Here you can see that the call as a whole has a region and the
170 function plus arguments are subregions of that. As a side-effect of
171 this, we get a lot of spurious errors around nested calls, in
172 particular when combined with `&mut` functions. For example, a call
173 like this one
174
175 self.foo(self.bar())
176
177 where both `foo` and `bar` are `&mut self` functions will always yield
178 an error.
179
180 Here is a more involved example (which is safe) so we can see what's
181 going on:
182
183 struct Foo { f: uint, g: uint }
184 ...
185 fn add(p: &mut uint, v: uint) {
186 *p += v;
187 }
188 ...
189 fn inc(p: &mut uint) -> uint {
190 *p += 1; *p
191 }
192 fn weird() {
193 let mut x: Box<Foo> = box Foo { ... };
194 'a: add(&mut (*x).f,
195 'b: inc(&mut (*x).f)) // (..)
196 }
197
198 The important part is the line marked `(..)` which contains a call to
199 `add()`. The first argument is a mutable borrow of the field `f`. The
200 second argument also borrows the field `f`. Now, in the current borrow
201 checker, the first borrow is given the lifetime of the call to
202 `add()`, `'a`. The second borrow is given the lifetime of `'b` of the
203 call to `inc()`. Because `'b` is considered to be a sublifetime of
204 `'a`, an error is reported since there are two co-existing mutable
205 borrows of the same data.
206
207 However, if we were to examine the lifetimes a bit more carefully, we
208 can see that this error is unnecessary. Let's examine the lifetimes
209 involved with `'a` in detail. We'll break apart all the steps involved
210 in a call expression:
211
212 'a: {
213 'a_arg1: let a_temp1: ... = add;
214 'a_arg2: let a_temp2: &'a mut uint = &'a mut (*x).f;
215 'a_arg3: let a_temp3: uint = {
216 let b_temp1: ... = inc;
217 let b_temp2: &'b = &'b mut (*x).f;
218 'b_call: b_temp1(b_temp2)
219 };
220 'a_call: a_temp1(a_temp2, a_temp3) // (**)
221 }
222
223 Here we see that the lifetime `'a` includes a number of substatements.
224 In particular, there is this lifetime I've called `'a_call` that
225 corresponds to the *actual execution of the function `add()`*, after
226 all arguments have been evaluated. There is a corresponding lifetime
227 `'b_call` for the execution of `inc()`. If we wanted to be precise
228 about it, the lifetime of the two borrows should be `'a_call` and
229 `'b_call` respectively, since the references that were created
230 will not be dereferenced except during the execution itself.
231
232 However, this model by itself is not sound. The reason is that
233 while the two references that are created will never be used
234 simultaneously, it is still true that the first reference is
235 *created* before the second argument is evaluated, and so even though
236 it will not be *dereferenced* during the evaluation of the second
237 argument, it can still be *invalidated* by that evaluation. Consider
238 this similar but unsound example:
239
240 struct Foo { f: uint, g: uint }
241 ...
242 fn add(p: &mut uint, v: uint) {
243 *p += v;
244 }
245 ...
246 fn consume(x: Box<Foo>) -> uint {
247 x.f + x.g
248 }
249 fn weird() {
250 let mut x: Box<Foo> = box Foo { ... };
251 'a: add(&mut (*x).f, consume(x)) // (..)
252 }
253
254 In this case, the second argument to `add` actually consumes `x`, thus
255 invalidating the first argument.
256
257 So, for now, we exclude the `call` lifetimes from our model.
258 Eventually I would like to include them, but we will have to make the
259 borrow checker handle this situation correctly. In particular, if
260 there is a reference created whose lifetime does not enclose
261 the borrow expression, we must issue sufficient restrictions to ensure
262 that the pointee remains valid.
263
264 ## Adding closures
265
266 The other significant complication to the region hierarchy is
267 closures. I will describe here how closures should work, though some
268 of the work to implement this model is ongoing at the time of this
269 writing.
270
271 The body of closures are type-checked along with the function that
272 creates them. However, unlike other expressions that appear within the
273 function body, it is not entirely obvious when a closure body executes
274 with respect to the other expressions. This is because the closure
275 body will execute whenever the closure is called; however, we can
276 never know precisely when the closure will be called, especially
277 without some sort of alias analysis.
278
279 However, we can place some sort of limits on when the closure
280 executes. In particular, the type of every closure `fn:'r K` includes
281 a region bound `'r`. This bound indicates the maximum lifetime of that
282 closure; once we exit that region, the closure cannot be called
283 anymore. Therefore, we say that the lifetime of the closure body is a
284 sublifetime of the closure bound, but the closure body itself is unordered
285 with respect to other parts of the code.
286
287 For example, consider the following fragment of code:
288
289 'a: {
290 let closure: fn:'a() = || 'b: {
291 'c: ...
292 };
293 'd: ...
294 }
295
296 Here we have four lifetimes, `'a`, `'b`, `'c`, and `'d`. The closure
297 `closure` is bounded by the lifetime `'a`. The lifetime `'b` is the
298 lifetime of the closure body, and `'c` is some statement within the
299 closure body. Finally, `'d` is a statement within the outer block that
300 created the closure.
301
302 We can say that the closure body `'b` is a sublifetime of `'a` due to
303 the closure bound. By the usual lexical scoping conventions, the
304 statement `'c` is clearly a sublifetime of `'b`, and `'d` is a
305 sublifetime of `'d`. However, there is no ordering between `'c` and
306 `'d` per se (this kind of ordering between statements is actually only
307 an issue for dataflow; passes like the borrow checker must assume that
308 closures could execute at any time from the moment they are created
309 until they go out of scope).
310
311 ### Complications due to closure bound inference
312
313 There is only one problem with the above model: in general, we do not
314 actually *know* the closure bounds during region inference! In fact,
315 closure bounds are almost always region variables! This is very tricky
316 because the inference system implicitly assumes that we can do things
317 like compute the LUB of two scoped lifetimes without needing to know
318 the values of any variables.
319
320 Here is an example to illustrate the problem:
321
322 fn identify<T>(x: T) -> T { x }
323
324 fn foo() { // 'foo is the function body
325 'a: {
326 let closure = identity(|| 'b: {
327 'c: ...
328 });
329 'd: closure();
330 }
331 'e: ...;
332 }
333
334 In this example, the closure bound is not explicit. At compile time,
335 we will create a region variable (let's call it `V0`) to represent the
336 closure bound.
337
338 The primary difficulty arises during the constraint propagation phase.
339 Imagine there is some variable with incoming edges from `'c` and `'d`.
340 This means that the value of the variable must be `LUB('c,
341 'd)`. However, without knowing what the closure bound `V0` is, we
342 can't compute the LUB of `'c` and `'d`! Any we don't know the closure
343 bound until inference is done.
344
345 The solution is to rely on the fixed point nature of inference.
346 Basically, when we must compute `LUB('c, 'd)`, we just use the current
347 value for `V0` as the closure's bound. If `V0`'s binding should
348 change, then we will do another round of inference, and the result of
349 `LUB('c, 'd)` will change.
350
351 One minor implication of this is that the graph does not in fact track
352 the full set of dependencies between edges. We cannot easily know
353 whether the result of a LUB computation will change, since there may
354 be indirect dependencies on other variables that are not reflected on
355 the graph. Therefore, we must *always* iterate over all edges when
356 doing the fixed point calculation, not just those adjacent to nodes
357 whose values have changed.
358
359 Were it not for this requirement, we could in fact avoid fixed-point
360 iteration altogether. In that universe, we could instead first
361 identify and remove strongly connected components (SCC) in the graph.
362 Note that such components must consist solely of region variables; all
363 of these variables can effectively be unified into a single variable.
364 Once SCCs are removed, we are left with a DAG. At this point, we
365 could walk the DAG in toplogical order once to compute the expanding
366 nodes, and again in reverse topological order to compute the
367 contracting nodes. However, as I said, this does not work given the
368 current treatment of closure bounds, but perhaps in the future we can
369 address this problem somehow and make region inference somewhat more
370 efficient. Note that this is solely a matter of performance, not
371 expressiveness.
372
373 # Skolemization and functions
374
375 One of the trickiest and most subtle aspects of regions is dealing
376 with the fact that region variables are bound in function types. I
377 strongly suggest that if you want to understand the situation, you
378 read this paper (which is, admittedly, very long, but you don't have
379 to read the whole thing):
380
381 http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/
382
383 Although my explanation will never compete with SPJ's (for one thing,
384 his is approximately 100 pages), I will attempt to explain the basic
385 problem and also how we solve it. Note that the paper only discusses
386 subtyping, not the computation of LUB/GLB.
387
388 The problem we are addressing is that there is a kind of subtyping
389 between functions with bound region parameters. Consider, for
390 example, whether the following relation holds:
391
392 fn(&'a int) <: |&'b int|? (Yes, a => b)
393
394 The answer is that of course it does. These two types are basically
395 the same, except that in one we used the name `a` and one we used
396 the name `b`.
397
398 In the examples that follow, it becomes very important to know whether
399 a lifetime is bound in a function type (that is, is a lifetime
400 parameter) or appears free (is defined in some outer scope).
401 Therefore, from now on I will write the bindings explicitly, using a
402 notation like `fn<a>(&'a int)` to indicate that `a` is a lifetime
403 parameter.
404
405 Now let's consider two more function types. Here, we assume that the
406 `self` lifetime is defined somewhere outside and hence is not a
407 lifetime parameter bound by the function type (it "appears free"):
408
409 fn<a>(&'a int) <: |&'a int|? (Yes, a => self)
410
411 This subtyping relation does in fact hold. To see why, you have to
412 consider what subtyping means. One way to look at `T1 <: T2` is to
413 say that it means that it is always ok to treat an instance of `T1` as
414 if it had the type `T2`. So, with our functions, it is always ok to
415 treat a function that can take pointers with any lifetime as if it
416 were a function that can only take a pointer with the specific
417 lifetime `&self`. After all, `&self` is a lifetime, after all, and
418 the function can take values of any lifetime.
419
420 You can also look at subtyping as the *is a* relationship. This amounts
421 to the same thing: a function that accepts pointers with any lifetime
422 *is a* function that accepts pointers with some specific lifetime.
423
424 So, what if we reverse the order of the two function types, like this:
425
426 fn(&'a int) <: <a>|&'a int|? (No)
427
428 Does the subtyping relationship still hold? The answer of course is
429 no. In this case, the function accepts *only the lifetime `&self`*,
430 so it is not reasonable to treat it as if it were a function that
431 accepted any lifetime.
432
433 What about these two examples:
434
435 fn<a,b>(&'a int, &'b int) <: <a>|&'a int, &'a int|? (Yes)
436 fn<a>(&'a int, &'a int) <: <a,b>|&'a int, &'b int|? (No)
437
438 Here, it is true that functions which take two pointers with any two
439 lifetimes can be treated as if they only accepted two pointers with
440 the same lifetime, but not the reverse.
441
442 ## The algorithm
443
444 Here is the algorithm we use to perform the subtyping check:
445
446 1. Replace all bound regions in the subtype with new variables
447 2. Replace all bound regions in the supertype with skolemized
448 equivalents. A "skolemized" region is just a new fresh region
449 name.
450 3. Check that the parameter and return types match as normal
451 4. Ensure that no skolemized regions 'leak' into region variables
452 visible from "the outside"
453
454 Let's walk through some examples and see how this algorithm plays out.
455
456 #### First example
457
458 We'll start with the first example, which was:
459
460 1. fn<a>(&'a T) <: <b>|&'b T|? Yes: a -> b
461
462 After steps 1 and 2 of the algorithm we will have replaced the types
463 like so:
464
465 1. fn(&'A T) <: |&'x T|?
466
467 Here the upper case `&A` indicates a *region variable*, that is, a
468 region whose value is being inferred by the system. I also replaced
469 `&b` with `&x`---I'll use letters late in the alphabet (`x`, `y`, `z`)
470 to indicate skolemized region names. We can assume they don't appear
471 elsewhere. Note that neither the sub- nor the supertype bind any
472 region names anymore (as indicated by the absence of `<` and `>`).
473
474 The next step is to check that the parameter types match. Because
475 parameters are contravariant, this means that we check whether:
476
477 &'x T <: &'A T
478
479 Region pointers are contravariant so this implies that
480
481 &A <= &x
482
483 must hold, where `<=` is the subregion relationship. Processing
484 *this* constrain simply adds a constraint into our graph that `&A <=
485 &x` and is considered successful (it can, for example, be satisfied by
486 choosing the value `&x` for `&A`).
487
488 So far we have encountered no error, so the subtype check succeeds.
489
490 #### The third example
491
492 Now let's look first at the third example, which was:
493
494 3. fn(&'a T) <: <b>|&'b T|? No!
495
496 After steps 1 and 2 of the algorithm we will have replaced the types
497 like so:
498
499 3. fn(&'a T) <: |&'x T|?
500
501 This looks pretty much the same as before, except that on the LHS
502 `&self` was not bound, and hence was left as-is and not replaced with
503 a variable. The next step is again to check that the parameter types
504 match. This will ultimately require (as before) that `&self` <= `&x`
505 must hold: but this does not hold. `self` and `x` are both distinct
506 free regions. So the subtype check fails.
507
508 #### Checking for skolemization leaks
509
510 You may be wondering about that mysterious last step in the algorithm.
511 So far it has not been relevant. The purpose of that last step is to
512 catch something like *this*:
513
514 fn<a>() -> fn(&'a T) <: || -> fn<b>(&'b T)? No.
515
516 Here the function types are the same but for where the binding occurs.
517 The subtype returns a function that expects a value in precisely one
518 region. The supertype returns a function that expects a value in any
519 region. If we allow an instance of the subtype to be used where the
520 supertype is expected, then, someone could call the fn and think that
521 the return value has type `fn<b>(&'b T)` when it really has type
522 `fn(&'a T)` (this is case #3, above). Bad.
523
524 So let's step through what happens when we perform this subtype check.
525 We first replace the bound regions in the subtype (the supertype has
526 no bound regions). This gives us:
527
528 fn() -> fn(&'A T) <: || -> fn<b>(&'b T)?
529
530 Now we compare the return types, which are covariant, and hence we have:
531
532 fn(&'A T) <: <b>|&'b T|?
533
534 Here we skolemize the bound region in the supertype to yield:
535
536 fn(&'A T) <: |&'x T|?
537
538 And then proceed to compare the argument types:
539
540 &'x T <: &'A T
541 &A <= &x
542
543 Finally, this is where it gets interesting! This is where an error
544 *should* be reported. But in fact this will not happen. The reason why
545 is that `A` is a variable: we will infer that its value is the fresh
546 region `x` and think that everything is happy. In fact, this behavior
547 is *necessary*, it was key to the first example we walked through.
548
549 The difference between this example and the first one is that the variable
550 `A` already existed at the point where the skolemization occurred. In
551 the first example, you had two functions:
552
553 fn<a>(&'a T) <: <b>|&'b T|
554
555 and hence `&A` and `&x` were created "together". In general, the
556 intention of the skolemized names is that they are supposed to be
557 fresh names that could never be equal to anything from the outside.
558 But when inference comes into play, we might not be respecting this
559 rule.
560
561 So the way we solve this is to add a fourth step that examines the
562 constraints that refer to skolemized names. Basically, consider a
563 non-directed verison of the constraint graph. Let `Tainted(x)` be the
564 set of all things reachable from a skolemized variable `x`.
565 `Tainted(x)` should not contain any regions that existed before the
566 step at which the skolemization was performed. So this case here
567 would fail because `&x` was created alone, but is relatable to `&A`.
568
569 ## Computing the LUB and GLB
570
571 The paper I pointed you at is written for Haskell. It does not
572 therefore considering subtyping and in particular does not consider
573 LUB or GLB computation. We have to consider this. Here is the
574 algorithm I implemented.
575
576 First though, let's discuss what we are trying to compute in more
577 detail. The LUB is basically the "common supertype" and the GLB is
578 "common subtype"; one catch is that the LUB should be the
579 *most-specific* common supertype and the GLB should be *most general*
580 common subtype (as opposed to any common supertype or any common
581 subtype).
582
583 Anyway, to help clarify, here is a table containing some
584 function pairs and their LUB/GLB:
585
586 ```
587 Type 1 Type 2 LUB GLB
588 fn<a>(&a) fn(&X) fn(&X) fn<a>(&a)
589 fn(&A) fn(&X) -- fn<a>(&a)
590 fn<a,b>(&a, &b) fn<x>(&x, &x) fn<a>(&a, &a) fn<a,b>(&a, &b)
591 fn<a,b>(&a, &b, &a) fn<x,y>(&x, &y, &y) fn<a>(&a, &a, &a) fn<a,b,c>(&a,&b,&c)
592 ```
593
594 ### Conventions
595
596 I use lower-case letters (e.g., `&a`) for bound regions and upper-case
597 letters for free regions (`&A`). Region variables written with a
598 dollar-sign (e.g., `$a`). I will try to remember to enumerate the
599 bound-regions on the fn type as well (e.g., `fn<a>(&a)`).
600
601 ### High-level summary
602
603 Both the LUB and the GLB algorithms work in a similar fashion. They
604 begin by replacing all bound regions (on both sides) with fresh region
605 inference variables. Therefore, both functions are converted to types
606 that contain only free regions. We can then compute the LUB/GLB in a
607 straightforward way, as described in `combine.rs`. This results in an
608 interim type T. The algorithms then examine the regions that appear
609 in T and try to, in some cases, replace them with bound regions to
610 yield the final result.
611
612 To decide whether to replace a region `R` that appears in `T` with a
613 bound region, the algorithms make use of two bits of information.
614 First is a set `V` that contains all region variables created as part
615 of the LUB/GLB computation. `V` will contain the region variables
616 created to replace the bound regions in the input types, but it also
617 contains 'intermediate' variables created to represent the LUB/GLB of
618 individual regions. Basically, when asked to compute the LUB/GLB of a
619 region variable with another region, the inferencer cannot oblige
620 immediately since the valuese of that variables are not known.
621 Therefore, it creates a new variable that is related to the two
622 regions. For example, the LUB of two variables `$x` and `$y` is a
623 fresh variable `$z` that is constrained such that `$x <= $z` and `$y
624 <= $z`. So `V` will contain these intermediate variables as well.
625
626 The other important factor in deciding how to replace a region in T is
627 the function `Tainted($r)` which, for a region variable, identifies
628 all regions that the region variable is related to in some way
629 (`Tainted()` made an appearance in the subtype computation as well).
630
631 ### LUB
632
633 The LUB algorithm proceeds in three steps:
634
635 1. Replace all bound regions (on both sides) with fresh region
636 inference variables.
637 2. Compute the LUB "as normal", meaning compute the GLB of each
638 pair of argument types and the LUB of the return types and
639 so forth. Combine those to a new function type `F`.
640 3. Replace each region `R` that appears in `F` as follows:
641 - Let `V` be the set of variables created during the LUB
642 computational steps 1 and 2, as described in the previous section.
643 - If `R` is not in `V`, replace `R` with itself.
644 - If `Tainted(R)` contains a region that is not in `V`,
645 replace `R` with itself.
646 - Otherwise, select the earliest variable in `Tainted(R)` that originates
647 from the left-hand side and replace `R` with the bound region that
648 this variable was a replacement for.
649
650 So, let's work through the simplest example: `fn(&A)` and `fn<a>(&a)`.
651 In this case, `&a` will be replaced with `$a` and the interim LUB type
652 `fn($b)` will be computed, where `$b=GLB(&A,$a)`. Therefore, `V =
653 {$a, $b}` and `Tainted($b) = { $b, $a, &A }`. When we go to replace
654 `$b`, we find that since `&A \in Tainted($b)` is not a member of `V`,
655 we leave `$b` as is. When region inference happens, `$b` will be
656 resolved to `&A`, as we wanted.
657
658 Let's look at a more complex one: `fn(&a, &b)` and `fn(&x, &x)`. In
659 this case, we'll end up with a (pre-replacement) LUB type of `fn(&g,
660 &h)` and a graph that looks like:
661
662 ```
663 $a $b *--$x
664 \ \ / /
665 \ $h-* /
666 $g-----------*
667 ```
668
669 Here `$g` and `$h` are fresh variables that are created to represent
670 the LUB/GLB of things requiring inference. This means that `V` and
671 `Tainted` will look like:
672
673 ```
674 V = {$a, $b, $g, $h, $x}
675 Tainted($g) = Tainted($h) = { $a, $b, $h, $g, $x }
676 ```
677
678 Therefore we replace both `$g` and `$h` with `$a`, and end up
679 with the type `fn(&a, &a)`.
680
681 ### GLB
682
683 The procedure for computing the GLB is similar. The difference lies
684 in computing the replacements for the various variables. For each
685 region `R` that appears in the type `F`, we again compute `Tainted(R)`
686 and examine the results:
687
688 1. If `R` is not in `V`, it is not replaced.
689 2. Else, if `Tainted(R)` contains only variables in `V`, and it
690 contains exactly one variable from the LHS and one variable from
691 the RHS, then `R` can be mapped to the bound version of the
692 variable from the LHS.
693 3. Else, if `Tainted(R)` contains no variable from the LHS and no
694 variable from the RHS, then `R` can be mapped to itself.
695 4. Else, `R` is mapped to a fresh bound variable.
696
697 These rules are pretty complex. Let's look at some examples to see
698 how they play out.
699
700 Out first example was `fn(&a)` and `fn(&X)`. In this case, `&a` will
701 be replaced with `$a` and we will ultimately compute a
702 (pre-replacement) GLB type of `fn($g)` where `$g=LUB($a,&X)`.
703 Therefore, `V={$a,$g}` and `Tainted($g)={$g,$a,&X}. To find the
704 replacement for `$g` we consult the rules above:
705 - Rule (1) does not apply because `$g \in V`
706 - Rule (2) does not apply because `&X \in Tainted($g)`
707 - Rule (3) does not apply because `$a \in Tainted($g)`
708 - Hence, by rule (4), we replace `$g` with a fresh bound variable `&z`.
709 So our final result is `fn(&z)`, which is correct.
710
711 The next example is `fn(&A)` and `fn(&Z)`. In this case, we will again
712 have a (pre-replacement) GLB of `fn(&g)`, where `$g = LUB(&A,&Z)`.
713 Therefore, `V={$g}` and `Tainted($g) = {$g, &A, &Z}`. In this case,
714 by rule (3), `$g` is mapped to itself, and hence the result is
715 `fn($g)`. This result is correct (in this case, at least), but it is
716 indicative of a case that *can* lead us into concluding that there is
717 no GLB when in fact a GLB does exist. See the section "Questionable
718 Results" below for more details.
719
720 The next example is `fn(&a, &b)` and `fn(&c, &c)`. In this case, as
721 before, we'll end up with `F=fn($g, $h)` where `Tainted($g) =
722 Tainted($h) = {$g, $h, $a, $b, $c}`. Only rule (4) applies and hence
723 we'll select fresh bound variables `y` and `z` and wind up with
724 `fn(&y, &z)`.
725
726 For the last example, let's consider what may seem trivial, but is
727 not: `fn(&a, &a)` and `fn(&b, &b)`. In this case, we'll get `F=fn($g,
728 $h)` where `Tainted($g) = {$g, $a, $x}` and `Tainted($h) = {$h, $a,
729 $x}`. Both of these sets contain exactly one bound variable from each
730 side, so we'll map them both to `&a`, resulting in `fn(&a, &a)`, which
731 is the desired result.
732
733 ### Shortcomings and correctness
734
735 You may be wondering whether this algorithm is correct. The answer is
736 "sort of". There are definitely cases where they fail to compute a
737 result even though a correct result exists. I believe, though, that
738 if they succeed, then the result is valid, and I will attempt to
739 convince you. The basic argument is that the "pre-replacement" step
740 computes a set of constraints. The replacements, then, attempt to
741 satisfy those constraints, using bound identifiers where needed.
742
743 For now I will briefly go over the cases for LUB/GLB and identify
744 their intent:
745
746 - LUB:
747 - The region variables that are substituted in place of bound regions
748 are intended to collect constraints on those bound regions.
749 - If Tainted(R) contains only values in V, then this region is unconstrained
750 and can therefore be generalized, otherwise it cannot.
751 - GLB:
752 - The region variables that are substituted in place of bound regions
753 are intended to collect constraints on those bound regions.
754 - If Tainted(R) contains exactly one variable from each side, and
755 only variables in V, that indicates that those two bound regions
756 must be equated.
757 - Otherwise, if Tainted(R) references any variables from left or right
758 side, then it is trying to combine a bound region with a free one or
759 multiple bound regions, so we need to select fresh bound regions.
760
761 Sorry this is more of a shorthand to myself. I will try to write up something
762 more convincing in the future.
763
764 #### Where are the algorithms wrong?
765
766 - The pre-replacement computation can fail even though using a
767 bound-region would have succeeded.
768 - We will compute GLB(fn(fn($a)), fn(fn($b))) as fn($c) where $c is the
769 GLB of $a and $b. But if inference finds that $a and $b must be mapped
770 to regions without a GLB, then this is effectively a failure to compute
771 the GLB. However, the result `fn<$c>(fn($c))` is a valid GLB.
772
773 */