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

Change handling of curried function types in capture checking #18131

Merged
merged 14 commits into from
Jul 15, 2023

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Jul 4, 2023

Implements the proposed treatment in cc-paths.

  • Capture sets of curried functions don't automatically propagate to the left
  • When computing the capture set of a reference, pick up capture sets along the span of curried functions
  • Drop the previous syntactic sugar for propagating captures left to right in curried function types.

@odersky odersky added the cc-experiment Intended to be merged with cc-experiment branch on origin label Jul 4, 2023
@odersky
Copy link
Contributor Author

odersky commented Jul 5, 2023

This is best reviewed commit by commit

odersky added 11 commits July 13, 2023 22:19
Some new comments, simplifications, syntax tweaks
And further simplifications and comments
Remove automatic insertion of captured in curried function types from left to right.
They were sometimes confusing and with deep capture sets are counter-productive now.
 - Don't widen actual in adaptBoxed if expected is a singleton type
 - Don't allow singleton types with capture sets (the theory does not
   allow them either)
Copy link
Contributor

@Linyxus Linyxus left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise LGTM!

adapted
else actual
if expected.isSingleton && actual.isSingleton then
println(i"shot $actual $expected")
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
println(i"shot $actual $expected")

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's deleted in follow-up commit in the other PR.

/** Reset `private` flags of parameter accessors so that we can refine them
* in Setup if they have non-empty capture sets. Special handling of some
* symbols defined for case classes.
/** - Reset `private` flags of parameter accessors so that we can refine them
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
/** - Reset `private` flags of parameter accessors so that we can refine them
/** - Reset `private` flags of parameter accessors so that we can refine them

@Linyxus
Copy link
Contributor

Linyxus commented Jul 14, 2023

Some meta-comments: currently only curried function closure stops capture propagation, but theoretically all function definitions could stop the propagation. For example:

val test1: Int ->{} Int ->{io} Int =
  x => y => {
    io.use()
    x + y
  }

val test2: Int ->{} Int ->{io} Int =
  x => {
    def f(y: Int): Int =
      io.use()
      x + y
    f
  }

By principle both cases should work but currently only the first one does. Could we make all function definitions stop the propagation of captures to allow cases like test2 as well?

@Linyxus
Copy link
Contributor

Linyxus commented Jul 14, 2023

After playing with more examples I discovered a soundness issue introduced by this PR:

trait Cap:
  def use(): Unit

def withCap[sealed T](op: (x: Cap^) => T): T = ???

trait Box:
  val get: () ->{} () ->{cap} Cap^

def main(): Unit =
  val leaked = withCap: (io: Cap^) =>
    class Foo extends Box, Pure:
      val get: () ->{} () ->{io} Cap^ = () => () => io
    new Foo
  val bad = leaked.get()().use()  // using a leaked capability

This is because curried function stops the captures from being propagated to the class's Env, so checking Foo against the Pure base passes (but it shouldn't). We probably need some special handling here: either tempering the capture propagation logic, or calculating the captured vars of a class "deeply" from its method types.

@Linyxus Linyxus assigned odersky and unassigned Linyxus Jul 14, 2023
@odersky odersky force-pushed the change-curried-captures branch from ffee8bd to c7a5350 Compare July 14, 2023 10:37
@odersky odersky merged commit ca19b46 into scala:main Jul 15, 2023
@odersky odersky deleted the change-curried-captures branch July 15, 2023 07:51
Linyxus added a commit that referenced this pull request Jul 22, 2023
Convert some standard library classes to capture checking. The converted
classes are represented as tests.
Initially, the `Iterator` and `IterableOnce` classes are converted.
UPDATE: By now, we have quite a few more, including List, ListBuffer,
View, and all their super classes and traits.

Also change capture checker to facilitate the conversion. The main
changes are about better interop with classes that are not (yet) capture
checked.

Based on #18131
@Kordyjan Kordyjan added this to the 3.4.0 milestone Aug 1, 2023
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.

3 participants