-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Exploit capture monotonicity in the apply rule? #14387
-
Captures have a monotonicity property. The references captured by the result of an evaluation are a subset of the references that captured by the evaluation itself. Specifically in a function call f x, the captures of the result must be subsumed by the union of the captures of f and the captures of x. This motivates a new, more permissive rule for apply:
E |- f: Cf (Ca Ta -> Cr Tr)
E |- a: Ca Ta
------------------------
E |- f a: Cr /\ {f, a} Tr
An example where the new rule is helpful is typing lazy lists. Here we have in slightly simplified form:
final class LazyCons[+T](val x: T, val xs: () => {*} LazyList[T]) extends LazyList[T]: this: {*} LazyList[T] => def isEmpty = false def head = x def tail: {this} LazyList[T] = xs()
With the old rule, xs() has capture set {*} so the typing of tail fails. But with the new rule, it would have
capture set {this.xs} /\ {*} = {this.xs}, and this.xs <: this by the path subsumption rule. So it checks out.
The idea is to replace the previous rule #13657 with the new rule, since it has a much clearer semantic motivation.
As a first step, the current implementation specializes the rule for the case where f is a tracked function and the capture set of the argument a is empty. That covers the LazyList example. We should consider generalizing to the case where the function arguments have non-empty capture sets, but that would make capture set computations more complex, so we should also evaluate the performance impact.
Beta Was this translation helpful? Give feedback.
All reactions
Replies: 3 comments
-
This new rule for application seems to make a lot of sense. It mirrors (app) from the reachability system, so it should be appropriate for us as well.
(削除) There's something slightly strange with the LazyCons example. Shouldn't the type of xs be {*} () => {*} LazyList[T]? Or do we have syntax sugar implemented and () => {*} LazyList[T] is the same as that type? (削除ここまで)
EDIT: OK, I just remembered that in fact we have syntax sugar like that, and we even discussed it before.
Other than that, the example makes sense to me. It's also further evidence that we want paths in capture sets.
Beta Was this translation helpful? Give feedback.
All reactions
-
One problem with the new rule is that the capture prediction lemma breaks down. In fact xs() will not contain a reference xs. We'd have to somehow interpret the xs in the capture set as "we got there through an application of xs", but it seems that would make reasoning more awkward. That might be a good reason to limit it to simple cases only, i.e require that all arguments in the application are pure.
One way to salvage the capture prediction lemma would be to treat every reference as a proxy for the set of primitive capabilities it could be instantiated with. Under that viewpoint it would be true that xs() and xs represent the same set, and that {f, a} is an upper bound of the set of capabilities captured by f a.
Beta Was this translation helpful? Give feedback.
All reactions
-
Yet another way to treat the example would be to extend paths to applications. i.e. this.xs() would be a path, and
this.xs() <: this.xs <: this. That would push it more towards full dependent typing.
Beta Was this translation helpful? Give feedback.