What this mans for the implementation

• Syntax and parsing rules for only-capabilities.
• A ClassifiedCapability base trait.
• Enforce restriction that a class cannot inherit two unrelated capability classes.
• A new capability class for only-capabilities.
• Implement captureSetOfInfo for only capabilities.
• The empty capability is x.only[Nothing]. It should have empty captureSetOfInfo.
• Well-formedness rules: only must refer to a classified capability class or to Nothing.
• Normalization rules:
  - it's *, then .only, then .rd,
  - multiple .only normalize to the smallest one if the classes are related,
  - multiple .only normalize to the empty capability if the classes are not related.
• define transitive capture set and cache it in a capability. The tcs does not exist if a capture set in the hierarchy is still an unsolved capture set variable.
• Add a classifier field to FreshCap and ResultCap.
• Modify capToFresh and toResultInResults so that the classifier field is correctly set.
• Using tcs, define when a capability is classified as a classifier class.
• A FreshCap with a classifier C can subsume only capabilities that are classified as C.
• Implement subsumption rules:
  - c.as[C] <: d if c <: d or c.as[D] <: empty
  - c.as[C] <: d.as[D] if c <: d and C derives from D
  - c <: d.as[D] if c <: d and c is classified as D
  - c.as[D] <: empty if tcs(c) consists of capabilities that all derive from classifier classes unrelated to D.

This looks like a lot of machinery to typecheck Try and Future. I there a simpler way? I have not found one yet. Can we ignore the problem? Then it seems we have to type Try(body) as T^{body}, which would ruin separation checking because then we cannot tell that body no longer can change anything because it has executed.

One possible generalization would be to have besides .as[C] also .asNot[C], or, with a different syntax: .as[!C]. This could be useful for instance to characterize the use set of a Try(body). It would be body.as[!Control] since all control capabilities have been caught by the Try.

One possible simplification is to specialize the treatment to control capabilites:

• Instead of @classifier traits have just two subtraits of Capability: Control and NonControl.
• Instead of c.as[C], have c.ctrl and c.nonctrl.
• Specialize the remaining rules accordingly.

This would make sense if we can convince ourselves that the only capability masking operations we envision mask specifically control capabilities. Can we?

One observation: .as can also be used to implement a new kind of capture set constraint:

 [C <: {cap.as[Mutable]}] // all elements of the set must be transitively `Mutable`.
 [C <: {cap.as[Sharable]} // all elements of the set must be transitively `Sharable`.
 [C <: {cap.as[Control]} // all elements of the set must be transitively `Control` capabilties.

And it is convenient to restrict capabilities of function types. For instance, when doing separation checking we might want to accept only functions over sharable capabilities. This can now be expressed:

A ->{cap.as[Sharable]} B

We could probably make this nicer by defining capture set aliases:

type sharable^ = {cap.as[Sharable]}
A ->{sharable} B

@bracevac Do you think this would work?

Overall I am coming to believe that this is a fundamental addition to capture checking that solves multiple expressiveness problems we had so far. So I tend to think we should do a trial implementation.

Maybe we need a more expressive language for what can go into an .as[...]. I mentioned already complement. We could also allow unions. Maybe we could write .as[Mutable, IOCapability], or .except[Control, Mutable]

This is a mechanism that enables limiting what can be closed over up to a certain threshold, which is very useful.

Without it, the next best thing one could do in the current system is using some form of branding through a variable in context (like we tried with the sub-regions example), but it's quite awkward and I don't think it scales well.

Classifiers seem to be less ad hoc, and it'd be good if we allowed users to extend the classifier hierarchy. I think classifiers subsume the advanced use cases from the 2nd-class values works. With finer-grained closure up to, we can emulate, e.g., Fig. 7 in the paper I linked:

@classifier trait Read extends Capability
@classifier trait ReadWrite extends Capability
trait File extends Capability:
 type R <: Read
 type RW <: ReadWrite
 given r: R
 given rw: RW
 // operations guarded by capability members
 def read(using this.R): Byte
 def write(using this.RW)(b: Byte): Unit
 
def withFile[U](block: File^ => U): U // unrestricted use of files & other capabilities
def parReduce[U](xs: Seq[U])(op: U ->{cap.only[Read]} U): U // only Read-classified allowed
withFile("foo.txt"): f =>
 parReduce(1 to 1000): (a, b) =>
 f.write(a) // error ReadWrite is excluded
 a + b + f.read() // ok
 f.write(0x42) // ok access unrestricted

We can understand the proposed forms in terms of set operations involving transitive capture closure, only being some kind of intersection (is there a connection to separation checking?),
and except as some kind of set difference, or intersection with a complement.

However, the .except form, as discussed offline, needs to be carefully restricted, especially if we permit user-defined extensions of the classifier hierarchy and separate compilation:

E.g.,

// File1.scala:
// Here, the universe of classifiers consists of the standard ones: Shareable, Mutable, Control
def mkPure(f: () ->{cap.except[Shareable,Mutable,Control] Unit): () ->{} Unit = 
 f // everything except all the known classifiers means nothing, so we are "pure"

can be subverted if we extend the classifiers elsewhere:

// File2.scala
@classifier Sneaky extends Capability
val s: Sneaky = ...
val fakePure: () -> Unit = 
 File1.mkPure(() => s.boom()) // ok!, since {s}.except[Shareable,Mutable,Control] = {s}