New Syntax for Capture Variables and Explicit Capture Polymorphism v3 #23063

bracevac · 2025-04-28T15:41:22Z

Closes #22490
Builds on #22725
Supersedes #22902

This syntax for capture variables and members caters to the view that "they are another kind", and most conventions we know from higher-kinded type parameters carry over.

A postfix ^ (analogous to [_]) indicates that a type parameter/member ranges over capture sets

def sayHi[C^](l: Logger^{C}) = l.log("hello world")

trait LList[T, C^]:
  type D^ >: C // or equivalently >: {C}
  val node: Ref[T^{D}]^

These variables can be bounded by capture-set literals:

trait Foo:
  type C^ 
  type D^ >: {logger} <: {logger, async, this.C}
  type E^ : Monad // error, context bounds are forbidden

Just as with higher-kinded type parameters, the kind is "contagious", and we can often avoid the hat if the bounds are concrete capture sets or other capture variables:

trait Foo:
  type C >: {} <: {cap}     // no hat needed
  type D >: C               // dito
  type E = {x,y,z}          // dito
  type F >: Object <: {cap} // error, ill-kinded

Capture variables will be erased if capture checking is turned off. In non-capture-checked code, they are essentially type variables within the interval >: caps.CapSet <: caps.CapSet. With capture checking turned on and without explicit bounds, the interval corresponds to >: caps.CapSet^{} <: caps.CapSet^{caps.cap}.

Tasks

Bullet-proof the "can avoid the hat" for binders scheme.
Grammar doc.
Update language reference.
Port new tests.
Clarify when and where to produce attachments.
Forbid nonsense intervals mixing capture sets and types.

bracevac · 2025-04-30T15:42:43Z

@odersky making these behave analogously to higher-kinded type parameters makes me wonder if

We should drop the lower bound CapSet and leave it at Nothing for capture-set variables? That makes parsing easier, especially scenarios where we are at liberty to omit the ^ and have some other cue that we are declaring a capture-set variable.
If yes, make CapSet truly its own kind by making it extend from AnyKind?

noti0na1 · 2025-04-30T18:59:15Z

We should drop the lower bound CapSet and leave it at Nothing for capture-set variables? That makes parsing easier, especially scenarios where we are at liberty to omit the ^ and have some other cue that we are declaring a capture-set variable.

If the lower bound of a capture variable is temprarily Noting during parsing, it is fine, but it must be bound by CapSet for both sides during or before typing. I don't know which way is easier, but I guess is doing in parser...

bracevac · 2025-04-30T19:51:47Z

It's not impossible to add the lower bound (& upper bound) during parsing. But if the mental model is "this is another kind", then the proposed scheme will be irregular for someone who is familiar with the syntax- and subtyping-rules for higher-kinded types in Scala.

noti0na1 · 2025-04-30T21:21:40Z

I don't think we should make a capture variable a real "kind"...

* Refrain from using a flag and in favor of an attachment. * Rule out context bounds entirely for capture vars.

bracevac · 2025-05-01T19:01:45Z

@noti0na1 ~~The old erroneous tests in tests/neg-custom-args/captures/capset-members.scala pass now when they shouldn't.~~
Nevermind, the problem was simply that the errors in the newly added test cases masked the old ones.

docs/_docs/reference/experimental/cc.md

We cannot post-process the typedef in typedTypeDef in the typer, because adaptation of the rhs prematurely sets the symbol info to the old bounds pre-expansion, which will be caught by checkBounds in posttyper. It is easier to mark the rhs as well and do the expansion in typedTypeBoundsTree.

bracevac · 2025-05-04T16:09:56Z

@odersky We cannot post-process in typedTypeDef in the typer, because adaptation of the unprocessed rhs prematurely sets the
symbol info to the old bounds pre-expansion, which will
be caught by checkBounds in posttyper.
It is easier to mark the rhs of the TypeDef with the attachment as well and do the expansion in
typedTypeBoundsTree before adaptation hits.

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

noti0na1 · 2025-05-05T14:31:21Z

I don't like there are so many special handling for capture sets when parsing a type dound/def.

Can we simplily parse a capture set as a "Type"?

Parser

When we parse typ() and see a {:

if it is followed by some kind of definition token, then return a structural type;
otherwise, parse as a capture set, and wrap it in CapSet with @retains.

If a type def has a hat, we add some attachment and use for latter. We don't care the rhs when parsing.

Typer

When completing a symbol for a type def:

If the type def has the attachment:
- if part of its bound hasEmptyTree, desugar it to corresponding CapSet;
- if the part of bound is not empty, check the type bounded by CapSet.
If the type def does not have the attachment, and both its bounds are not empty and bounded by CapSet, then treat the type as capture valure as well.

type C1^ // => capture type C1 >: CapSet <: CapSet^
type C2^ <: {a} // => capture type C2 >: CapSet <: CapSet^{a}
type C3 <: {a} // => regular type C3 >: Nothing <: CapSet^{a}
type C4 >: {} <: {a} // => capture type C4 >: CapSet <: CapSet^{a}
type C5 = {a} // => capture type C5 >: CapSet^{a} <: CapSet^{a}

type C6^ >: {} <: {a} // => capture type, but redundant hat
type C7^ = {a} // => capture type, but redundant hat

type C8 >: C1 <: C2 // => capture type C8 >: C1<: C2

def f[C^] = ???

f[{a}]
type S = {a}
f[{S}] // ok
f[S]  // ok, just looks like a substitution

bracevac · 2025-05-05T15:21:35Z

I don't like there are so many special handling for capture sets when parsing a type dound/def.

Can we simplily parse a capture set as a "Type"?

Right now, it's tailored to exactly the usage contexts where we expect to be able to write literal capture sets. Making this a new case for general types would also permit expressions like {a,b,c} => {d,e,f}, no? I'm not sure we want to go into that direction. Maybe @odersky can weigh in.

noti0na1 · 2025-05-05T15:26:50Z

Making this a new case for general types would also permit expressions like {a,b,c} => {d,e,f}

I'd say a CapSet^{...} is just a general type. Even if we prevent literal capture set in function type, we cannot prevent using a capture variable, like C1 => C2.

Since we don't have any value for CapSet, I think this is fine.

bracevac · 2025-05-05T15:36:05Z

type C3 <: {a} // => regular type C3 >: Nothing <: CapSet^{a}

Well, hence my comment on making it truly like a new kind. If we upper-bound
a type with a higher-kinded type, it's itself higher-kinded.
For higher-kinded types, Nothing is the default lower bound. But I think we agreed on letting these guys range over >: CapSet <: CapSet^. Plus, @odersky is in favor of forbidding nonsense intervals like >: Nothing <: CapSet. I would need to see a compelling actual usecase that would necessitate that as well as the higher degrees of freedom where capture sets can occur.

f[{a}]
type S = {a}
f[{S}] // ok
f[S]  // ok, just looks like a substitution

I'm pretty sure these all work right now. No?

noti0na1 · 2025-05-05T15:45:41Z

Well, if we really want to relax the rule for type C3 <: {a}, we can say in the Namer: if one side is bound by CapSet, then another side must also be bound by CapSet, and turning left Nothing into CapSet and right Any into CapSet^.

My example just want to show allowing a set should be equal to allowing a capture variable in bound.

bracevac · 2025-05-06T11:58:46Z

After discussing with @odersky, we are not going to deviate from the current scheme and will permit the sets only in those specific circumstances. While the general approach and code structure will remain as is, I appreciate feedback on specific details and possible simplifications - just not the broader simplification that was proposed, which we feel is too general for this case.

noti0na1 · 2025-05-06T12:05:26Z

OK, I will add another point to my proposal: if we want to support capture set intersection in the future, for example {a, b} & C. If we only consider top level literal sets at certain places, this forbids general usage of sets as types and makes difficult to support this form. On the other hand, with my scheme, it is straightforward.

odersky

Only minor changes needed. Generally looks good!

odersky · 2025-05-09T10:30:14Z

docs/_docs/internals/syntax.md

 NamesAndTypes     ::=  NameAndType {‘,’ NameAndType}
 NameAndType       ::=  id ':' Type
+CaptureSet        ::=  ‘{’ CaptureRef {‘,’ CaptureRef} ‘}’                      -- under captureChecking
+CaptureRef        ::=  { SimpleRef ‘.’ } SimpleRef [‘*’] [‘.’ ‘rd’]             -- under captureChecking
+                    |  [ { SimpleRef ‘.’ } SimpleRef ‘.’ ] id                   -- under captureChecking


Suggested change

| [ { SimpleRef ‘.’ } SimpleRef ‘.’ ] id -- under captureChecking

This line is now redundant. We needed it only to support the final ^ which is now gone.

I see it was already removed in Parser.

odersky · 2025-05-09T12:17:36Z

docs/_docs/reference/experimental/cc.md

+inaccessible after invoking its `concat` method. This is achieved with mutation and separation tracking which are
+currently in development.
+
+Finally, analogously to type parameters, we can lower- and upper-bound capability parameters where the bounds consist of concrete capture sets:


This are probably quite exotic use cases. My concern is we muddle the message how capabilties would usually be applied, and we scare people away. Suggestion: Let's make a separate page (only linked from here, not sidebar.yml) on "advanced use cases of capabilties".

odersky · 2025-05-09T12:18:03Z

docs/_docs/reference/experimental/cc.md

+Since `caps.cap` is the top element for subcapturing, we could have also left out the
+upper bound: `type Cap^ >: {cudaMalloc, cudaFree}`.
+
+We conclude with a more advanced example, showing how capability members and paths to these members can prevent leakage


Same thing here. Let's move this to the adavnced use cases page.

odersky · 2025-05-09T15:24:02Z

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

     */
    def argTypes(namedOK: Boolean, wildOK: Boolean, tupleOK: Boolean): List[Tree] =
-      def argType() =
-        val t = typ()
+      inline def wildCardCheck(inline gen: Tree): Tree =


gen does does not have to be inline. It's evaluated before anything else anyway. I think wildcardCheck does not have to be inline either. The JVM will inline this anyway. Inlining is useful if it prevents boxing or closure creation. Here neither happens.

odersky · 2025-05-09T15:25:48Z

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

      else if tupleOK && isIdent && in.lookahead.isColon && sourceVersion.enablesNamedTuples then
-        commaSeparated(() => namedElem())
+        commaSeparated(() => nameAndType()) // TODO: can capture-set variables occur here?


I don't think they can.

odersky · 2025-05-09T15:27:13Z

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

-      if (in.token == tok) { in.nextToken(); toplevelTyp() }
+      if (in.token == tok) then
+        in.nextToken()
+        if Feature.ccEnabled && (in.token == LBRACE && !isDclIntroNext) then


Suggested change

if Feature.ccEnabled && (in.token == LBRACE && !isDclIntroNext) then

if Feature.ccEnabled && in.token == LBRACE && !isDclIntroNext then

odersky · 2025-05-09T15:33:59Z

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

+      if isLowerBound && refs.isEmpty then // lower bounds with empty capture sets become a pure CapSet
+        Select(scalaDot(nme.caps), tpnme.CapSet)
+      else
+        makeRetaining(Select(scalaDot(nme.caps), tpnme.CapSet), refs, tpnme.retains)


You can re-use concreteCapsType here.

odersky · 2025-05-09T15:37:31Z

tests/neg-custom-args/captures/capset-members.scala

 import caps.*

 trait Abstract[X^]:
-  type C >: X <: CapSet^
+  type C^ >: {X}


Would C >: {X} also work here? If yes, let's test that it does.

odersky · 2025-05-09T15:37:42Z

tests/neg-custom-args/captures/capset-bound.scala

@@ -5,14 +5,14 @@ class IO
 case class File(io: IO^)

 def test(io1: IO^, io2: IO^) =
-  def f[C >: CapSet^{io1} <: CapSet^](file: File^{C^}) = ???
+  def f[C^ >: {io1}](file: File^{C}) = ???


Would C >: {io1} also work here? If yes, let's test that it does.

odersky · 2025-05-09T15:42:19Z

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -715,6 +715,10 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
        && ctx.owner.owner.unforcedDecls.lookup(tree.name).exists
    then // we are in the arguments of a this(...) constructor call
      errorTree(tree, em"$tree is not accessible from constructor arguments")
+    else if name.isTermName && ctx.mode.is(Mode.InCaptureSet) then


I assume this will be changed later by Yaoyu's commit?

I think so, I inherited this change from his earlier PR removing ^ in for capture refs to capture variables.

bracevac force-pushed the capset-syntax3 branch from 9e1754b to ff07e02 Compare April 29, 2025 18:46

bracevac marked this pull request as ready for review April 30, 2025 15:34

bracevac assigned bracevac and odersky and unassigned bracevac Apr 30, 2025

bracevac requested review from noti0na1 and odersky April 30, 2025 15:38

noti0na1 and others added 10 commits May 1, 2025 20:55

Remove unnecessary ^ in capture set syntax.

151ebd9

Tight the condition for retrying InCaptureSet

baea3e3

Forget to reuse the bit

0667639

New capture-vars syntax, "higher-kinds" style

ff068c6

Tests for the new capture-variable syntax

67708cb

Update CC language reference

169dd69

Update internal syntax.md

57a1b73

Make ^ optional in more scenarios for cap vars

22a79e2

Fix pretty-printing of capture variables

1cc8590

Desugar capture vars in typer instead of parser

c8ef6d1

* Refrain from using a flag and in favor of an attachment. * Rule out context bounds entirely for capture vars.

bracevac force-pushed the capset-syntax3 branch from 331ab8a to c8ef6d1 Compare May 1, 2025 18:57

bishabosha reviewed May 1, 2025

View reviewed changes

docs/_docs/reference/experimental/cc.md Outdated Show resolved Hide resolved

bracevac added 3 commits May 2, 2025 13:19

Fixes in language reference and tests cases

630a20f

Rule out nonsensical bounds for capture variables

9658555

noti0na1 reviewed May 5, 2025

View reviewed changes

compiler/src/dotty/tools/dotc/parsing/Parsers.scala Outdated Show resolved Hide resolved

Move capvars checks to typer & allow variances

5004928

odersky reviewed May 9, 2025

View reviewed changes

odersky assigned bracevac and unassigned odersky May 9, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New Syntax for Capture Variables and Explicit Capture Polymorphism v3 #23063

New Syntax for Capture Variables and Explicit Capture Polymorphism v3 #23063

bracevac commented Apr 28, 2025 •

edited

Loading

bracevac commented Apr 30, 2025

noti0na1 commented Apr 30, 2025

bracevac commented Apr 30, 2025

noti0na1 commented Apr 30, 2025

bracevac commented May 1, 2025 •

edited

Loading

bracevac commented May 4, 2025

noti0na1 commented May 5, 2025 •

edited

Loading

bracevac commented May 5, 2025

noti0na1 commented May 5, 2025

bracevac commented May 5, 2025

noti0na1 commented May 5, 2025

bracevac commented May 6, 2025 •

edited

Loading

noti0na1 commented May 6, 2025

odersky left a comment

odersky May 9, 2025

odersky May 9, 2025

odersky May 9, 2025

odersky May 9, 2025

odersky May 9, 2025

odersky May 9, 2025

odersky May 9, 2025

odersky May 9, 2025

odersky May 9, 2025

odersky May 9, 2025

odersky May 9, 2025

bracevac May 9, 2025

	if Feature.ccEnabled && (in.token == LBRACE && !isDclIntroNext) then
	if Feature.ccEnabled && in.token == LBRACE && !isDclIntroNext then

New Syntax for Capture Variables and Explicit Capture Polymorphism v3 #23063

Are you sure you want to change the base?

New Syntax for Capture Variables and Explicit Capture Polymorphism v3 #23063

Conversation

bracevac commented Apr 28, 2025 • edited Loading

Tasks

bracevac commented Apr 30, 2025

noti0na1 commented Apr 30, 2025

bracevac commented Apr 30, 2025

noti0na1 commented Apr 30, 2025

bracevac commented May 1, 2025 • edited Loading

bracevac commented May 4, 2025

noti0na1 commented May 5, 2025 • edited Loading

Parser

Typer

bracevac commented May 5, 2025

noti0na1 commented May 5, 2025

bracevac commented May 5, 2025

noti0na1 commented May 5, 2025

bracevac commented May 6, 2025 • edited Loading

noti0na1 commented May 6, 2025

odersky left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bracevac commented Apr 28, 2025 •

edited

Loading

bracevac commented May 1, 2025 •

edited

Loading

noti0na1 commented May 5, 2025 •

edited

Loading

bracevac commented May 6, 2025 •

edited

Loading