Introduction

Capabilities are extremely versatile. They can express concepts from many different domains. Exceptions, continuations, I/O, mutation, information flow, security permissions, are just some examples, the list goes on.

Sometimes it is important to restrict, or: classify what kind of capabilities are expected or returned in a context. For instance, we might want to allow only control capabilities such as CanThrows or boundary Labels but no other capabilities. Or might want to allow mutation, but no other side effects. This is achieved by having a capability class extend a classifier.

For instance, the scala.caps package defines a classifier trait called Control, like this:

trait Control extends SharedCapability, Classifier

The Gears library then defines a capability class Async which extends Control.

import language.experimental.captureChecking
import caps.*
trait Async extends Control

Unlike normal inheritance, classifiers also restrict the capture set of a capability. For instance, say we have a function

import language.experimental.captureChecking
import caps.*
trait Async extends Control
def f(using async: Async^) = ()

(the ^ is as usual redundant here since Async is a capability trait). Then we have the guarantee that any actual async argument can only capture capabilities that have types extending Control. No other capabilities such as mutation or I/O are allowed.

A class or trait becomes a classifier by extending directly the marker trait caps.Classifier. So with the definitions above, Control is a classifier trait, but Async is not, since it extends Classifier only indirectly, through Control.

Classifiers are unique: a class cannot extend directly or transitively at the same time two unrelated classifier traits. So if a class transitively extends two classifier traits C1 and C2 then one of them must be a subtrait of the other.

Predefined Classifiers

The caps object defines the Classifier trait itself and some traits that extend it:

trait Classifier

sealed trait Capability

trait SharedCapability extends Capability, Classifier
trait Control extends SharedCapability, Classifier

trait ExclusiveCapability extends Capability
trait Unscoped extends ExclusiveCapability, Classifier

Here is a graph showing the hierarchy of predefined capability traits. Classifier traits are underlined.

              Capability
              /        \
             /          \
            /            \
           /              \
 SharedCapability     ExclusiveCapability
 ----------------            |
        |                    |
        |                    |
     Control              Unscoped
     -------              --------

At the top of the hierarchy, we distinguish between shared and exclusive capabilities in two traits SharedCapability and ExclusiveCapability. All capability classes we have seen so far are shared. ExclusiveCapability is a base trait for capabilities that are checked for anti-aliasing restrictions with the rules governed by separation checking. Separation checking is currently an optional extension of capture checking, enabled by a different language import. Since Capability is a sealed trait, all capability classes are either shared or exclusive. SharedCapability is a classifier, but ExclusiveCapability is not. Therefore, exclusive capabilities can have shared capabilities in their capture set but not vice versa.

Control capabilities are shared. This means they cannot directly or indirectly capture exclusive capabilities such as capabilities that control access to mutable state. Typical Control capabilities are:

• Labels that enable to return from a boundary,
• CanThrow capabilities that enable throwing exceptions, or
• Async capabilities that allow to suspend.

These are all expressed by having their capability classes extend Control.

Classifier Restriction

Consider the following problem: The Try.apply method takes in its body parameter a computation, and runs it while catching any exceptions or boundary.break aborts. The exception or break will be re-issued when calling the get method of a Try object. What should a capability-aware signature of Try be?

The body passed to Try.apply can have arbitrary effects, so it can retain arbitrary capabilities. Yet the resulting Try object will retain only those capabilities of body which are classified as Control. So the signature of Try.apply should look like this:

import language.experimental.captureChecking
import caps.*
class Try[+T]
object Try:
  def apply[T](body: => T): Try[T]^{body.only[Control]} = ???

Note a new form of capability in the result's capture set: body.only[Control]. This is called a restricted capability. The general form of a restricted capability is c.only[A] where

• c is a regular, unrestricted capability
• A is a classifier trait.

When substituting a capability set for the underlying capability, we drop all capabilities that are known to be unrelated to the classifier. For instance, say we have an actual body { expr } that uses a capture set {io, async} where

• io is an IO capability, where IO is assumed to extend SharedCapability but not Control.
• async is a Control capability.

Then the result of Try { expr } would have type Try^{async}. We drop io since io's type is a Capability class that does not extend Control.

If expr would use an additional capability proc: () => Unit, then proc would also show up in the result capture set. Since proc is fully effect-polymorphic, we can't exclude that it retains Control capabilities, so we have to keep it in the restricted capture set. These elements are shown together in the following example:

class IO extends caps.SharedCapability
class Async extends caps.Control

def test(io: IO, async: Async, proc: () => Unit) =
  val r = Try:
    // code accessing `io`, `async`, and `proc` and returning an `Int.
  val _: Try[Int]^{async, proc} = r

Classifier Exclusion

Restriction keeps the capabilities that fall under a classifier; exclusion does the reverse, keeping everything except those. Suppose a method runs its argument on a separate thread. That argument must not capture a Control capability such as a boundary.Label or a CanThrow, since each is bound to the stack of the thread that created it; invoking one from another thread would jump into a different thread's stack. Capabilities of every other kind are admitted. We express this with an excluded capability:

import language.experimental.captureChecking
import caps.*
def runOnNewThread[T](body: () ->{any.except[Control]} T): T = ???

The general form of an excluded capability is c.except[A] where

• c is a regular capability, possibly carrying an only restriction
• A is a classifier trait.

c.except[A] stands for the parts of c that are not classified as A or a subclass of A. A capability x is covered by c.except[A] only if x is covered by c and x is known to be unrelated to the classifier A. For instance, take a FileSystem capability whose classifier IO is a sibling of Control:

import language.experimental.captureChecking
import caps.*
def runOnNewThread[T](body: () ->{any.except[Control]} T): T = ???
trait IO extends SharedCapability, Classifier
class FileSystem extends IO:
  def read(): Unit = ()

A closure over a FileSystem is accepted, since IO is unrelated to Control:

import language.experimental.captureChecking
import caps.*
def runOnNewThread[T](body: () ->{any.except[Control]} T): T = ???
trait IO extends SharedCapability, Classifier
class FileSystem extends IO:
  def read(): Unit = ()
def onIO(fs: FileSystem^) = runOnNewThread(() => fs.read())

A closure that might retain a Control capability is rejected — whether it captures an Async (which is a Control), an unclassified function value, or a capability classified only as SharedCapability (of which Control is a sub-classifier):

import language.experimental.captureChecking
import caps.*
def runOnNewThread[T](body: () ->{any.except[Control]} T): T = ???
import language.experimental.captureChecking
import caps.*
trait Async extends Control
def onControl(async: Async^)            = runOnNewThread(() => async.toString)  // error
def onUnclassified(proc: () => Unit)    = runOnNewThread(() => proc())          // error
def onShared(shared: SharedCapability^) = runOnNewThread(() => shared.toString) // error

Restriction and exclusion can be combined: c.only[A].except[B] keeps those capabilities of c that are classified as A but not as B. If B covers all of A, the result is the empty capture set. Several exclusions can be chained — c.except[A].except[B] removes both — and their order does not matter.

Subcapturing relates excluded capabilities as follows, where B is a subtrait of classifier trait A:

{c.except[A]} <: {c}
{c.only[A].except[B]} <: {c.only[A]}
{c.except[A]} <: {c.except[B]}

The last rule holds since excluding a larger classifier A removes more capabilities than excluding a smaller one B. Exclusions of unrelated classifiers are not comparable.

The top classifier

A projection can also name Any, the top above all classifiers. Any is not itself a classifier trait, but it is accepted as the argument of .only and .except, where it stands for all capabilities. This gives two limiting cases:

• c.only[Any] is the identity restriction: it keeps all of c, so {c.only[Any]} is the same as {c}.
• c.except[Any] is the empty exclusion: it removes all of c, so {c.except[Any]} is the empty capture set.