New Syntax for Capture Variables and Explicit Capture Polymorphism v2

[bracevac]

Closes #22490
Builds on #22725
Supersedes #22758

This aim of this PR is reducing the clunkyness of the explicit capture polymorphism syntax following internal discussions.

Syntax Overview

Below is a short summary of the syntax. For more extensive usage examples, the CC language reference and the test cases in this PR are a good starting point. For the grammar, refer to the updated syntax.md.

Capture-set parameters

Capture-set parameters can be defined alongside type parameters within angle brackets,
they are preceded by the soft-keyword cap (not to be confused with the universal capture set caps.cap).

def apply[cap C, T, U](f: T ->{C} U)(x: T): U = f(x)

cap-qualified parameters accept capture sets as arguments, i.e., we can regard those parameters as ranging over the universe of capture sets which are finite sets of references to capabilities written in the usual curly braces:

apply[{io},Int,Int](i => io.println(i); i*i)(7)

Just as for type arguments, capture-set arguments can be often inferred.

Similarly, capture-set parameters can receive upper and/or lower bounds which are capture sets:

def apply[cap C >: {io} <: {io,network}, cap D <: {C}, cap E >: {C,D}, T, U] ...

Capture-set members

We also support capture-set members much in the same way as type members:

trait Foo:
  cap type C >: {io} <: {io,network}
  cap type D = {network}

as well as paths in capture sets:

def poly(f: Foo)[cap C <: {f.D}](g: () ->{C} Unit): Unit = g()

Variations

Moving forward, is this a good syntax?

Capture-set notation: For regularity, capture sets must be always written in curly braces. But should there be exceptions? For examples, do we really need to write singletons in braces all the time?

def poly(f: Foo)[cap C <: f.D]

trait Foo:
  cap type C >: io <: {io, network}
  cap type D = network

Consider type refinements:

def useFoo(foo: Foo {cap type C = {io}}): Logger^{foo.C} = ???

Are we overdosing on braces?

Marking capture-parameters and -members:
Declaring them with the soft modifier cap clearly delineates them from
ordinary type variables. If this is too wordy, we could partly switch back to the
old syntax design (a post-fix hat ^) for a more terse syntax:

def poly(f: Foo)[C^ <: f.D]

trait Foo:
  type C^ >: io <: {io, network}
  type D^ = network

def useFoo(foo: Foo {type C^ = io}): Logger^{foo.C} = ???

However, we expect explicit polymorphism for captures to be fairly rare in practice,
so maybe this is not a big deal if we write the cap modifier from time to time?

Should being a capture-parameter be contagious?

Tasks

• Nice to have: partial applications and compatibility with named type arguments

import language.experimental.namedTypeArguments
foo[{a,b}]
foo[cap D = {x}]

• Rebase on Separation checking for product types #22539 and patch all tests.
• Document the parser changes for capture checking in the internal syntax.md.
• Add specialized syntax error messages for cap lists & co. (make separate issue)
• Remove the old [C^] syntax for good.
• Make cap members and lists pretty-printed (with option to turn off). (separate issue, let's wait for under-the-hood changes to the capset representation)
• Let parser mark capture variables with some attachment to be used by later phases.
• Update CC language reference with the new syntax.

[odersky]

I think it would be good to open a thread on contributors to discuss the new syntax. That way, p[eople can weigh in with opinions and proposals.

[noti0na1]

Overall LGTM

[odersky]

Looking at the test cases I am now less sure this is the best syntax. In particular I find the cap modifier a bit jarring, and it's also not immediately obvious to me where and why we need {...} around arguments.

We should try to get some representative test cases, evaluate how common we believe they will be, and compare different syntaxes with each other. That's what we did for the givens before we settled on one syntax. We could have that discussion thread here on the PR or on contributors.

[bracevac]

Looking at the test cases I am now less sure this is the best syntax. In particular I find the cap modifier a bit jarring, and it's also not immediately obvious to me where and why we need {...} around arguments.

We discussed this. They are needed around all capture arguments and bounds of capture variables. The previous design allowed dropping them for singleton sets, but we didn't want it. It's regular, though I have to say, while patching the examples, I tended to subconsciously go back to braceless singletons from time to time only to be surprised by syntax errors...

What should be the alternative for cap as a modifier? We somehow have to mark those type variables which are capture variables. Does that mean we are going back to [C^]? I find it too cryptic compared to [cap C]. Though I find member declarations cap type C somewhat wordy compared to just cap C or type C^.

We should try to get some representative test cases, evaluate how common we believe they will be, and compare different syntaxes with each other. That's what we did for the givens before we settled on one syntax. We could have that discussion thread here on the PR or on contributors.

🫡 on it!

[noti0na1]

I would say the interval of a capture variable is: >: {} <: {cap}, to hide the internal CapSet.

In a separate paragraph, we can point out CapSet is a special internal type to carry capture sets, and cap X is de-sugared to X >: CapSet <: CapSet^

[bracevac]

Addressed in 1de50f6

[noti0na1]

I don't think a fixed bound is a good example to illustrate the polymorphism...

[bracevac]

The point is to show that bounds can be annotated. Polymorphism has been introduced up to this point.