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

[bracevac]

Right now, the syntax for explicit capture polymorphism is quite noisy and irregular:

val b: Bar^ = ???
def capturePolyDef[A^,
                   B >: CapSet <: A,
                   C >: CapSet <: CapSet^{B^},
                   D >: CapSet <: C,
                   E >: CapSet <: CapSet^{D^},
                   F >: CapSet <: CapSet^{A^,b},
                   X >: CapSet <: CapSet^{F^,D^},
                   Y >: CapSet^{F^} <: CapSet^{F^,A^,b},
                   Z >: CapSet^{b} <: CapSet^{b,Y^}] = ???

For example:

• There are too many hats ^ and it's not always clear when they are needed, e.g., all the type variables in the example are capture variables, but only A's declaration carries the ^ (which is a shorthand for A >: CapSet <: CapSet^.

• There's two ways to write down a capture variable's bounds, e.g., E's upper bound is CapSet^{D^} but could equivalently be written as just D.

• Lots of CapSet mentions everywhere, which seems a bit clunky to express simple subset relationships.

• TODO: how does/will Capybara affect capture set notations?

Let's use this issue to track ideas for making the notations more palatable.

[bracevac]

One idea that came up in offline discussions is reusing the context bound notation for declaring a capture variable:

def foo[A:CapSet] = ???

with the aim that this notation internally desugars into the current encoding

def foo[A >: CapSet <: CapSet^] = ???

This will require special treatment of CapSet in context bound position, because context bounds usually take a type parameter, but CapSet is parameterless.

How should this extend to declarations of capture variables which are sub-/supercaptures of A ? With regular context bound notation, it would look like

def foo[A: CapSet, B <: A : CapSet, C >: B <: A : CapSet] = ???

We'd expect this to desugar into the existing scheme

def foo[A >: CapSet <: CapSet^, B >: CapSet <: A, C >: B <: A] = ???

while making sure that omitted lower (upper) bounds are CapSet (CapSet^).

That seems still a bit verbose, should we instead aim for CapSet being contagious?

def foo[A: CapSet, B <: A, C >: B <: A] = ???

I.e., just by being subtyping-related to the declared CapSet variable A, we expect B and C to be implicitly CapSet as well?

[natsukagami]

Just for reference, if the example were written in Rust with lifetimes this is how it would look like:

// assuming a lifetime 'bb was predeclared,
// since we cannot mention lifetime of a variable directly
let b: &'bb Bar = ???
fn capturePolyDef<'a,
                   'b: 'a,
                   'c: 'b,
                   'd: 'c,
                   'e: 'd,
                   'f: 'a + 'bb,
                   'x: 'f + 'd,
                   'y, // lower bound constraints must come in `where` clauses
                   'z>() 
where 
  'y: 'f + 'a + 'bb,
  'f: 'y,
  'z: 'bb + 'y,
  'b: 'z,
{
  todo!()
}

Notably the pesky backticks appear everywhere, and the lack of direct lower bound constraints (which we have built-in with subtyping constraints)

[bracevac]

At one of the recent LAMP meetings, we gravitated towards this form:

def foo[A: CapSet, B <: A : CapSet, C >: B <: A : CapSet] = ???

But then we switch from "too many hats" to "too many CapSets", e.g.,

def foo[A: CapSet, B <: CapSet^{A,x,y,z} : CapSet] = ???

which seems not the most ideal.

Regarding

This will require special treatment of CapSet in context bound position, because context bounds usually take a type parameter, but CapSet is parameterless.

we can build on the proposed mechanism for Singleton. That would give us a better story for having a term-level reference to the type-level capture variables that can be mentioned in capture sets.