@@ -249,61 +249,114 @@ there is a reference created whose lifetime does not enclose
249
249
the borrow expression, we must issue sufficient restrictions to ensure
250
250
that the pointee remains valid.
251
251
252
- ## Modeling closures
253
-
254
- Integrating closures properly into the model is a bit of
255
- work-in-progress. In an ideal world, we would model closures as
256
- closely as possible after their desugared equivalents. That is, a
257
- closure type would be modeled as a struct, and the region hierarchy of
258
- different closure bodies would be completely distinct from all other
259
- fns. We are generally moving in that direction but there are
260
- complications in terms of the implementation.
261
-
262
- In practice what we currently do is somewhat different. The basis for
263
- the current approach is the observation that the only time that
264
- regions from distinct fn bodies interact with one another is through
265
- an upvar or the type of a fn parameter (since closures live in the fn
266
- body namespace, they can in fact have fn parameters whose types
267
- include regions from the surrounding fn body). For these cases, there
268
- are separate mechanisms which ensure that the regions that appear in
269
- upvars/parameters outlive the dynamic extent of each call to the
270
- closure:
271
-
272
- 1 . Types must outlive the region of any expression where they are used.
273
- For a closure type ` C ` to outlive a region ` 'r ` , that implies that the
274
- types of all its upvars must outlive ` 'r ` .
275
- 2 . Parameters must outlive the region of any fn that they are passed to.
276
-
277
- Therefore, we can -- sort of -- assume that any region from an
278
- enclosing fns is larger than any region from one of its enclosed
279
- fn. And that is precisely what we do: when building the region
280
- hierarchy, each region lives in its own distinct subtree, but if we
281
- are asked to compute the ` LUB(r1, r2) ` of two regions, and those
282
- regions are in disjoint subtrees, we compare the lexical nesting of
283
- the two regions.
284
-
285
- * Ideas for improving the situation:* (FIXME #3696 ) The correctness
286
- argument here is subtle and a bit hand-wavy. The ideal, as stated
287
- earlier, would be to model things in such a way that it corresponds
288
- more closely to the desugared code. The best approach for doing this
289
- is a bit unclear: it may in fact be possible to * actually* desugar
290
- before we start, but I don't think so. The main option that I've been
291
- thinking through is imposing a "view shift" as we enter the fn body,
292
- so that regions appearing in the types of fn parameters and upvars are
293
- translated from being regions in the outer fn into free region
294
- parameters, just as they would be if we applied the desugaring. The
295
- challenge here is that type inference may not have fully run, so the
296
- types may not be fully known: we could probably do this translation
297
- lazilly, as type variables are instantiated. We would also have to
298
- apply a kind of inverse translation to the return value. This would be
299
- a good idea anyway, as right now it is possible for free regions
300
- instantiated within the closure to leak into the parent: this
301
- currently leads to type errors, since those regions cannot outlive any
302
- expressions within the parent hierarchy. Much like the current
303
- handling of closures, there are no known cases where this leads to a
304
- type-checking accepting incorrect code (though it sometimes rejects
305
- what might be considered correct code; see rust-lang/rust #22557 ), but
306
- it still doesn't feel like the right approach.
252
+ ## Adding closures
253
+
254
+ The other significant complication to the region hierarchy is
255
+ closures. I will describe here how closures should work, though some
256
+ of the work to implement this model is ongoing at the time of this
257
+ writing.
258
+
259
+ The body of closures are type-checked along with the function that
260
+ creates them. However, unlike other expressions that appear within the
261
+ function body, it is not entirely obvious when a closure body executes
262
+ with respect to the other expressions. This is because the closure
263
+ body will execute whenever the closure is called; however, we can
264
+ never know precisely when the closure will be called, especially
265
+ without some sort of alias analysis.
266
+
267
+ However, we can place some sort of limits on when the closure
268
+ executes. In particular, the type of every closure ` fn:'r K ` includes
269
+ a region bound ` 'r ` . This bound indicates the maximum lifetime of that
270
+ closure; once we exit that region, the closure cannot be called
271
+ anymore. Therefore, we say that the lifetime of the closure body is a
272
+ sublifetime of the closure bound, but the closure body itself is unordered
273
+ with respect to other parts of the code.
274
+
275
+ For example, consider the following fragment of code:
276
+
277
+ 'a: {
278
+ let closure: fn:'a() = || 'b: {
279
+ 'c: ...
280
+ };
281
+ 'd: ...
282
+ }
283
+
284
+ Here we have four lifetimes, ` 'a ` , ` 'b ` , ` 'c ` , and ` 'd ` . The closure
285
+ ` closure ` is bounded by the lifetime ` 'a ` . The lifetime ` 'b ` is the
286
+ lifetime of the closure body, and ` 'c ` is some statement within the
287
+ closure body. Finally, ` 'd ` is a statement within the outer block that
288
+ created the closure.
289
+
290
+ We can say that the closure body ` 'b ` is a sublifetime of ` 'a ` due to
291
+ the closure bound. By the usual lexical scoping conventions, the
292
+ statement ` 'c ` is clearly a sublifetime of ` 'b ` , and ` 'd ` is a
293
+ sublifetime of ` 'd ` . However, there is no ordering between ` 'c ` and
294
+ ` 'd ` per se (this kind of ordering between statements is actually only
295
+ an issue for dataflow; passes like the borrow checker must assume that
296
+ closures could execute at any time from the moment they are created
297
+ until they go out of scope).
298
+
299
+ ### Complications due to closure bound inference
300
+
301
+ There is only one problem with the above model: in general, we do not
302
+ actually * know* the closure bounds during region inference! In fact,
303
+ closure bounds are almost always region variables! This is very tricky
304
+ because the inference system implicitly assumes that we can do things
305
+ like compute the LUB of two scoped lifetimes without needing to know
306
+ the values of any variables.
307
+
308
+ Here is an example to illustrate the problem:
309
+
310
+ fn identify<T>(x: T) -> T { x }
311
+
312
+ fn foo() { // 'foo is the function body
313
+ 'a: {
314
+ let closure = identity(|| 'b: {
315
+ 'c: ...
316
+ });
317
+ 'd: closure();
318
+ }
319
+ 'e: ...;
320
+ }
321
+
322
+ In this example, the closure bound is not explicit. At compile time,
323
+ we will create a region variable (let's call it ` V0 ` ) to represent the
324
+ closure bound.
325
+
326
+ The primary difficulty arises during the constraint propagation phase.
327
+ Imagine there is some variable with incoming edges from ` 'c ` and ` 'd ` .
328
+ This means that the value of the variable must be `LUB('c,
329
+ 'd)` . However, without knowing what the closure bound ` V0` is, we
330
+ can't compute the LUB of ` 'c ` and ` 'd ` ! Any we don't know the closure
331
+ bound until inference is done.
332
+
333
+ The solution is to rely on the fixed point nature of inference.
334
+ Basically, when we must compute ` LUB('c, 'd) ` , we just use the current
335
+ value for ` V0 ` as the closure's bound. If ` V0 ` 's binding should
336
+ change, then we will do another round of inference, and the result of
337
+ ` LUB('c, 'd) ` will change.
338
+
339
+ One minor implication of this is that the graph does not in fact track
340
+ the full set of dependencies between edges. We cannot easily know
341
+ whether the result of a LUB computation will change, since there may
342
+ be indirect dependencies on other variables that are not reflected on
343
+ the graph. Therefore, we must * always* iterate over all edges when
344
+ doing the fixed point calculation, not just those adjacent to nodes
345
+ whose values have changed.
346
+
347
+ Were it not for this requirement, we could in fact avoid fixed-point
348
+ iteration altogether. In that universe, we could instead first
349
+ identify and remove strongly connected components (SCC) in the graph.
350
+ Note that such components must consist solely of region variables; all
351
+ of these variables can effectively be unified into a single variable.
352
+ Once SCCs are removed, we are left with a DAG. At this point, we
353
+ could walk the DAG in topological order once to compute the expanding
354
+ nodes, and again in reverse topological order to compute the
355
+ contracting nodes. However, as I said, this does not work given the
356
+ current treatment of closure bounds, but perhaps in the future we can
357
+ address this problem somehow and make region inference somewhat more
358
+ efficient. Note that this is solely a matter of performance, not
359
+ expressiveness.
307
360
308
361
### Skolemization
309
362
0 commit comments