Skip to content
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

Special rule for {this} in capture sets of class members #13657

Merged
merged 1 commit into from
Nov 3, 2021

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Oct 2, 2021

Consider the lazylists.scala test in pos-custom-args/captures:

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 PR, 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:

      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 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

@odersky odersky added the cc-experiment Intended to be merged with cc-experiment branch on origin label Oct 2, 2021
@odersky
Copy link
Contributor Author

odersky commented Oct 2, 2021

One might be tempted to try the following definition of tail in Mapped:

      def tail: {xs, f} LazyList[B] = xs.tail.map(f)  // error: bad override

That would fail the override check sincetail's type in Mapped is then not seen as a subtype of the tail in LazyList[A].

@odersky odersky force-pushed the this-cc-in-members branch 2 times, most recently from b546307 to c568038 Compare October 2, 2021 19:46
@odersky
Copy link
Contributor Author

odersky commented Oct 4, 2021

Happy to report that the original version with LazyCons now also compiles under the new rules

@odersky
Copy link
Contributor Author

odersky commented Oct 5, 2021

Alex found a counter-example, which means we need to restrict the expected type widening to final classes.
See map5 in neg-customargs/captures/lazylists2.scala

@odersky odersky force-pushed the this-cc-in-members branch from b8a3608 to 5f407b3 Compare October 5, 2021 10:24
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
@odersky odersky force-pushed the this-cc-in-members branch from 5f407b3 to 6fc8c98 Compare October 13, 2021 09:14
@odersky odersky merged commit c9a275c into scala:cc-experiment Nov 3, 2021
@odersky odersky deleted the this-cc-in-members branch November 3, 2021 10:43
odersky added a commit to dotty-staging/dotty that referenced this pull request Jan 31, 2022
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.
odersky added a commit to dotty-staging/dotty that referenced this pull request Jan 31, 2022
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.
odersky added a commit to dotty-staging/dotty that referenced this pull request Feb 9, 2022
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.
odersky added a commit that referenced this pull request Feb 25, 2022
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.
odersky added a commit that referenced this pull request Mar 6, 2022
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.
odersky added a commit that referenced this pull request Mar 26, 2022
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.
odersky added a commit that referenced this pull request Apr 28, 2022
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.
odersky added a commit that referenced this pull request May 18, 2022
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.
odersky added a commit that referenced this pull request May 29, 2022
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.
odersky added a commit that referenced this pull request Jul 26, 2022
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.
odersky added a commit that referenced this pull request Jul 26, 2022
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.
odersky added a commit that referenced this pull request Jul 26, 2022
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.
odersky added a commit that referenced this pull request Aug 8, 2022
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.
odersky added a commit that referenced this pull request Aug 17, 2022
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.
odersky added a commit to dotty-staging/dotty that referenced this pull request Aug 29, 2022
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cc-experiment Intended to be merged with cc-experiment branch on origin
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant