New Syntax for Capture Variables and Explicit Capture Polymorphism v3

[bracevac]

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]

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

1. 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.
2. If yes, make CapSet truly its own kind by making it extend from AnyKind?

[noti0na1]

1. 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]

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]

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

[bracevac]

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

[bracevac]

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

[noti0na1]

I don't see any reason to disallow it.

[noti0na1]

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:

1. 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.
2. 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]

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]

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]

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]

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]

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]

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.