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

New Syntax for Capture Variables and Explicit Capture Polymorphism #22758

Draft
wants to merge 8 commits into
base: main
Choose a base branch
from

Conversation

bracevac
Copy link
Contributor

@bracevac bracevac commented Mar 9, 2025

[skip community_build]

Closes #22490
Builds on #22725

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

  • Support dedicated parameter lists for capture variables of the form [cap B, A <: {B,x,y,z} ].
    • Adds more degrees of freedom how to syntactically represent capture variables.
    • Under the hood we can have term names for capture variables. The typer will see them as term names, and the capture checker will treat them as types (addressed by Remove ^ in capture set syntax #22725).
      Morally, capture variables are both terms and types (analogy: companion objects).
    • Better backwards compatibility story, as these parameters are clearly delineated from other kinds now.
    • Capture parameter lists may immediately follow normal type parameter lists:
def foo[T][cap C <: {c,d,e}, D ][X <: T] = ???
def bar[cap C] = ???
  • Implement more liberal rules for capture parameter lists in curried functions.
def foo2[cap C][cap D <: C] = ???   // illegal
def bar2[cap C]()[cap D <: C] = ??? // legal
// lambdas:
[cap C] => [cap D] => (x: T^{C,D}) => x // this is NOT planned, instead use
[cap C,D] => (x: T^{C,D}) => x // legal
[T <: Foo] => [cap D <: T.C] => (x: Foo^{D}) => x // TODO should also be legal

We might still in the future support uninterrupted curried lists of explicit capture-set parameters.

  • Support the same new syntax for capture members:
trait Foo:
  cap C <: {x,y,z}
  cap D >: x <: C
  cap E = {x,C,D}
  • We specify bounds and definitions using the intuitive set notation. Note the absence of the hat ^ symbol for capture variables.
  • Singleton sets can be written with or without the curly braces, i.e., cap C <: x is the same as cap C <: {x}.
  • cap members and parameters cannot be higher-kinded, i.e., they take no type-level parameters.
  • cap members and parameters may have context bounds, like ordinary type parameters.
  • Support for cap parameter lists in higher-kinded types.
trait Foo[cap C] // legal
trait Bar:
  type X[cap C]  // legal
  cap Y[T]       // illegal
trait Baz extends Bar:
  override type X = [cap C] =>> Any // type lambdas not planned
  • Syntax for applying functions to explicit capture parameters.
    • Inspired by using for context parameters, we permit applying explicit capture sets with cap (assume foo's signature from above):
foo[cap A, D]
  • Partial applications are currently not planned, but may be supported in the future and named capture arguments coincidentally "just work":
import language.experimental.namedTypeArguments
foo[cap {a,b}]
foo[cap D = {x}]

Standard type inference applies to other type parameters (such as T and X of foo).

  • Extended syntax of capture set bounds (maybe, not planned now).

    • For control capabilities, we might want intersections def foo3[cap A, B, C <: A & B] = ???
    • However, we don't want/need the union type notation def foo4[cap A, B, C <: A | B], since we can always use the set notation {A,B}.
    • Generally, we do not want arbitrary type operators appearing in the bounds of capture-variable declarations.
  • 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.

  • Remove the old [C^] syntax for good.

  • Make cap members and lists pretty-printed (with option to turn off).

  • Let parser mark capture variables with some attachment to be used by later phases.

@bracevac
Copy link
Contributor Author

Just rebased on latest main

@bracevac
Copy link
Contributor Author

bracevac commented Mar 13, 2025

After some deliberation, it's better to put the cap lists at the end of standard type parameter lists: [T,U, cap C, D, E <: {C,D}] and make cap a soft modifier: trait Foo { cap type C }. Otherwise, we'd have to support curried type parameter lists for classes and traits: trait Foo[T][cap U] { } which are weird.

Note: since declared parameters can depend on subsequent parameters, there is no loss in expressivity, e.g., we can still support trait Bar[Future^{C}, cap C].

Applications:
Given def foo[T,U,cap C, cap D]() = ...
Initially:
foo[A,B,{x}, {y}] need to supply full list.
Eventually:
foo[{x}, {y}] but need to teach type inference first.

However, in argument positions need to disambiguate between structural types and refinement types, as well as object {}.

We drop the convenience that singletons do not require braces.
It always has to be in braces.

TODO: make example file with various syntax ideas.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

CC: Better End-User Syntax for Declaring and Mentioning Capture Variables
3 participants