What this mans for the implementation

• Syntax and parsing rules foronly-capabilities.
• AClassifiedCapability base trait.
• Enforce restriction that a class cannot inherit two unrelated capability classes.
• A new capability class foronly-capabilities.
• ImplementcaptureSetOfInfo foronly capabilities.
• The empty capability isx.only[Nothing]. It should have emptycaptureSetOfInfo.
• Well-formedness rules:only must refer to a classified capability class or toNothing.
• 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. Thetcs does not exist if a capture set in the hierarchy is still an unsolved capture set variable.
• Add aclassifier field toFreshCap andResultCap.
• ModifycapToFresh andtoResultInResults so that the classifier field is correctly set.
• Usingtcs, define when a capability is classified as a classifier class.
• A FreshCap with a classifierC can subsume only capabilities that are classified asC.
• Implement subsumption rules:
  -c.as[C] <: d ifc <: d orc.as[D] <: empty
  -c.as[C] <: d.as[D] ifc <: d andC derives fromD
  -c <: d.as[D] ifc <: d andc is classified asD
  -c.as[D] <: empty iftcs(c) consists of capabilities that all derive from classifier classes unrelated toD.

This looks like a lot of machinery to typecheckTry andFuture. I there a simpler way? I have not found one yet. Can we ignore the problem? Then it seems we have to typeTry(body) asT^{body}, which would ruin separation checking because then we cannot tell thatbody 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 aTry(body). It would bebody.as[!Control] since all control capabilities have been caught by theTry.

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

• Instead of@classifier traits have just two subtraits ofCapability:Control andNonControl.
• Instead ofc.as[C], havec.ctrl andc.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:

typesharable^= {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. Ithink classifiers subsume the advanced use cases from the2nd-class values works. With finer-grainedclosure up to, we can emulate, e.g., Fig. 7 in the paper I linked:

@classifiertraitReadextendsCapability@classifiertraitReadWriteextendsCapabilitytraitFileextendsCapability:typeR<:ReadtypeRW<:ReadWritegivenr:Rgivenrw:RW// operations guarded by capability membersdefread(usingthis.R):Bytedefwrite(usingthis.RW)(b:Byte):UnitdefwithFile[U](block:File^=>U):U// unrestricted use of files & other capabilitiesdefparReduce[U](xs:Seq[U])(op:U->{cap.only[Read]}U):U// only Read-classified allowedwithFile("foo.txt"): f=>  parReduce(1 to1000): (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?),
andexcept 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, ControldefmkPure(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@classifierSneakyextendsCapabilityvals:Sneaky= ...valfakePure: ()->Unit=File1.mkPure(()=> s.boom())// ok!, since {s}.except[Shareable,Mutable,Control] = {s}