-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Special rule for {this} in capture sets of class members
#13657
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
|
One might be tempted to try the following definition of That would fail the override check since |
b546307 to
c568038
Compare
|
Happy to report that the original version with |
|
Alex found a counter-example, which means we need to restrict the expected type widening to final classes. |
b8a3608 to
5f407b3
Compare
Consider the lazylists.scala test in pos-custom-args/captures:
```scala
class CC
type Cap = {*} CC
trait LazyList[+A]:
this: ({*} LazyList[A]) =>
def isEmpty: Boolean
def head: A
def tail: {this} LazyList[A]
object LazyNil extends LazyList[Nothing]:
def isEmpty: Boolean = true
def head = ???
def tail = ???
extension [A](xs: {*} LazyList[A])
def map[B](f: {*} A => B): {xs, f} LazyList[B] =
class Mapped extends LazyList[B]:
this: ({xs, f} Mapped) =>
def isEmpty = false
def head: B = f(xs.head)
def tail: {this} LazyList[B] = xs.tail.map(f) // OK
new Mapped
```
Without this commit, the second to last line is an error since the right hand side
has capture set `{xs, f}` but the required capture set is `this`.
To fix this, we widen the expected type of the rhs `xs.tail.map(f)` from `{this}` to
`{this, f, xs}`. That is, we add the declared captures of the self type to the expected
type. The soundness argument for doing this is as follows:
Since `tail` does not have parameters, the only thing it could capture are references that the
receiver `this` captures as well. So `xs` and `f` must come via `this`. For instance, if
the receiver `xs` of `xs.tail` happens to be pure, then `xs.tail` is pure as well.
On the other hand, in the neg test `lazylists1.scala` we add the following line to `Mapped`:
```scala
def concat(other: {f} LazyList[A]): {this} LazyList[A] = ??? : ({xs, f} LazyList[A]) // error
```
Here, we cannot widen the expected type from `{this}` to `{this, xs, f}` since the result of concat
refers to `f` independently of `this`, namely through its parameter `other`. Hence, if `ys: {f} LazyList[String]`
then
```
LazyNil.concat(ys)
```
still refers to `f` even though `LazyNil` is pure. But if we would accept the definition of `concat`
above, the type of `LazyNil.concat(ys)` would be `LazyList[String]`, which is unsound.
The current implementation widens the expected type of class members if the class member does not
have tracked parameters. We could potentially refine this to say we widen with all references in
the expected type that are not subsumed by one of the parameter types.
## Changes:
### Refine rule for this widening
We now widen the expected type of the right hand side of a class member as follows:
Add all references of the declared type of this that are not subsumed by a capture set
of a parameter type.
### Do expected type widening only in final classes
Alex found a counter-example why this is required. See map5 in
neg-customargs/captures/lazylists2.scala
5f407b3 to
6fc8c98
Compare
The following two rules replace scala#13657: 1. Exploit capture monotonicity in the apply rule, as discussed in scala#14387. 2. A rule to make typing nested classes more flexible as discussed in scala#14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace scala#13657: 1. Exploit capture monotonicity in the apply rule, as discussed in scala#14387. 2. A rule to make typing nested classes more flexible as discussed in scala#14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace scala#13657: 1. Exploit capture monotonicity in the apply rule, as discussed in scala#14387. 2. A rule to make typing nested classes more flexible as discussed in scala#14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace #13657: 1. Exploit capture monotonicity in the apply rule, as discussed in #14387. 2. A rule to make typing nested classes more flexible as discussed in #14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
The following two rules replace scala#13657: 1. Exploit capture monotonicity in the apply rule, as discussed in scala#14387. 2. A rule to make typing nested classes more flexible as discussed in scala#14390. There's also a bug fix where we now enforce a previously missing subcapturing relationship between the capture set of parent of a class and the capture set of the class itself. Clearly a class captures all variables captured by one of its parent classes.
Consider the lazylists.scala test in pos-custom-args/captures:
Without this PR, the second to last line is an error since the right hand side
has capture set
{xs, f}but the required capture set isthis.To fix this, we widen the expected type of the rhs
xs.tail.map(f)from{this}to{this, f, xs}. That is, we add the declared captures of the self type to the expectedtype. The soundness argument for doing this is as follows:
Since
taildoes not have parameters, the only thing it could capture are references that thereceiver
thiscaptures as well. Soxsandfmust come viathis. For instance, ifthe receiver
xsofxs.tailhappens to be pure, thenxs.tailis pure as well.On the other hand, in the neg test
lazylists1.scalawe add the following line toMapped:Here, we cannot widen the expected type from
{this}to{this, xs, f}since the result of concatrefers to
findependently ofthis, namely through its parameterother. Hence, ifys: {f} LazyList[String]then
still refers to
feven thoughLazyNilis pure. But if we would accept the definition ofconcatabove, the type of
LazyNil.concat(ys)would beLazyList[String], which is unsound.The implementation in 7ba98d3 widens the expected type of class members if the class member does not
have tracked parameters. We can refine this to say we widen with all references in
the expected type that are not subsumed by one of the parameter types. This is done in d6a2659