Capability Classifiers
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 CanThrow
s or boundary Label
s 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
.
trait Async extends Control
Unlike normal inheritance, classifiers also restrict the capture set of a capability. For instance, say we have a function
def f(using async: Async^) = body
(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, Classifier
trait Mutable extends ExclusiveCapability, Classifier
Here is a graph showing the hierarchy of predefined classifier traits:
Capability
/ \
/ \
/ \
/ \
SharedCapability ExclusiveCapability
| |
| |
| |
| |
Control Mutable
At the top of the hierarchy, we distinguish between shared and exclusive capabilities in two classifier traits SharedCapability
and ExclusiveCapability
. All capability classes we have seen so far are shared. ExclusiveCapability
is a base trait for capabilities that allow only un-aliased access to the data they represent, 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.
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:
Label
s that enable to return from aboundary
,CanThrow
capabilities that enable throwing exceptions, orAsync
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:
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 capabilityA
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 anIO
capability, where IO is assumed to extendSharedCapability
but notControl
.async
is aControl
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