Hello!
As we are gearing up for the next big milestone of the experimental capture-checking feature, we are looking for community feedback on a new syntax for explicit capture polymorphism, which is a complimentary mechanism for the default implicit capture polymorphism.
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 example, 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?
Discussion topic
The purpose of this thread is discussing the syntax design for explicit capture polymorphism and soliciting community feedback. We are looking forward to thoughts and suggestions about the proposed syntax.