docs/_docs/internals/exclusive-capabilities.md
Language design draft
A capability is called
SharedCapabilityWe introduce a new trait
trait Mutable extends ExclusiveCapability, Classifier
It is used as a base trait for types that define update methods using
a new soft modifier update.
update can only be used in classes or objects extending Mutable. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending Mutable may access exclusive capabilities only if they are defined locally or passed to it in parameters.
Example:
class Ref(init: Int) extends Mutable:
private var current = init
def get: Int = current
update def put(x: Int): Unit = current = x
Here, put needs to be declared as an update method since it accesses the exclusive write capability of the variable current in its environment.
update can also be used on an inner class of a class or object extending Mutable. It gives all code in the class the right
to access exclusive capabilities in the class environment. Normal classes
can only access exclusive capabilities defined in the class or passed to it in parameters.
object Registry extends Mutable:
var count = 0
update class Counter:
update def next: Int =
count += 1
count
Normal method members of Mutable classes cannot call update methods. This is indicated since accesses in the callee are recorded in the caller. So if the callee captures exclusive capabilities so does the caller.
An update method cannot implement or override a normal method, whereas normal methods may implement or override update methods. Since methods such as toString or == inherited from Object are normal methods, it follows that none of these methods may be implemented as an update method.
The apply method of a function type is also a normal method, hence Mutable classes may not implement a function type with an update method as the apply method.
A type is called a mutable if it extends Mutable and it has an update method or an update class as non-private member or constructor.
When we create an instance of a mutable type we always add cap to its capture set. For instance, if class Ref is declared as shown previously then new Ref(1) has type Ref[Int]^{cap}.
Restriction: A non-mutable type cannot be downcast by a pattern match to a mutable type.
Definition: A class is read_only if the following conditions are met:
Restriction: If a class or trait extends Mutable all its parent classes or traits must either extend Mutable or be read-only.
The idea is that when we upcast a reference to a type extending Mutable to a type that does not extend Mutable, we cannot possibly call a method on this reference that uses an exclusive capability. Indeed, by the previous restriction this class must be a read-only class, which means that none of the code implemented
in the class can access exclusive capabilities on its own. And we
also cannot override any of the methods of this class with a method
accessing exclusive capabilities, since such a method would have
to be an update method and update methods are not allowed to override regular methods.
Example:
Consider trait IterableOnce from the standard library.
trait IterableOnce[+T] extends Mutable:
def iterator: Iterator[T]^{this}
update def foreach(op: T => Unit): Unit
update def exists(op: T => Boolean): Boolean
...
The trait is a mutable type with many update methods, among them foreach and exists. These need to be classified as update because their implementation in the subtrait Iterator uses the update method next.
trait Iterator[T] extends IterableOnce[T]:
def iterator = this
def hasNext: Boolean
update def next(): T
update def foreach(op: T => Unit): Unit = ...
update def exists(op; T => Boolean): Boolean = ...
...
But there are other implementations of IterableOnce that are not mutable types (even though they do indirectly extend the Mutable trait). Notably, collection classes implement IterableOnce by creating a fresh
iterator each time one is required. The mutation via next() is then restricted to the state of that iterator, whereas the underlying collection is unaffected. These implementations would implement each update method in IterableOnce by a normal method without the update modifier.
trait Iterable[T] extends IterableOnce[T]:
def iterator = new Iterator[T] { ... }
def foreach(op: T => Unit) = iterator.foreach(op)
def exists(op: T => Boolean) = iterator.exists(op)
Here, Iterable is not a mutable type since it has no update method as member.
All inherited update methods are (re-)implemented by normal methods.
Note: One might think that we don't need a base trait Mutable since in any case
a mutable type is defined by the presence of update methods, not by what it extends. In fact the importance of Mutable is that it defines the other methods as read-only methods that cannot access exclusive capabilities. For types not extending Mutable, this is not the case. For instance, the apply method of a function type is not an update method and the type itself does not extend Mutable. But apply may well be implemented by
a method that accesses exclusive capabilities.
If x is an exclusive capability of a type extending Mutable, x.rd is its associated, shared read-only capability.
A top capability is either cap or shared.
Meaning of ^:
The meaning of ^ and => is the same as before:
C^ means C^{cap}.A => B means (A -> B)^{cap}.Implicitly added capture sets
A reference to a type extending trait Mutable gets an implicit capture set {cap.rd} provided no explicit capture set is given.
For instance, a matrix multiplication method can be expressed as follows:
class Matrix(nrows: Int, ncols: Int) extends Mutable:
update def update(i: Int, j: Int, x: Double): Unit = ...
def apply(i: Int, j: Int): Double = ...
def mul(a: Matrix, b: Matrix, c: Matrix^): Unit =
// multiply a and b, storing the result in c
Here, a and b are implicitly read-only, and c's type has capture set cap. I.e. with explicit capture sets this would read:
def mul(a: Matrix^{cap.rd}, b: Matrix^{cap.rd}, c: Matrix^{cap}): Unit
Separation checking will then make sure that a and b must be different from c.
As the previous example showed, we would like to use a Mutable type such as Array or Matrix in two permission levels: read-only and unrestricted. A standard technique is to invent a type qualifier such as "read-only" or "mutable" to indicate access permissions. What we would like to do instead is to combine the qualifier with the capture set of a type. So we
distinguish two kinds of capture sets: regular and read-only. Read-only sets can contain only shared capabilities.
Internally, in the discussion that follows we use a label after the set to indicate its mode. {...}_ is regular and {...}rd is read-only. We could envisage source language to specify read-only sets, e.g. something like
{io, async}.rd
But in almost all cases we don't need an explicit mode in source code to indicate the kind of capture set, since the contents of the set itself tell us what kind it is. A capture set is assumed to be read-only if it is on a
type extending Mutable and it contains only shared capabilities, otherwise it is assumed to be regular.
The read-only function ro maps capture sets to read-only capture sets. It is defined pointwise on capabilities as follows:
ro ({ x1, ..., xn } _) = { ro(x1), ..., ro(xn) }ro(x) = x if x is sharedro(x) = x.rd if x is exclusiveSubcapturing has to take the mode of capture sets into account. We let m stand for arbitrary modes.
Rule (sc-var) comes in two variants. If x is defined as S^C then
{x, xs} m <: (C u {xs}) m{x.rd, xs} m <: (ro(C) u {xs}) mThe subset rule works only between sets of the same kind:
C _ <: C _ u {x}C rd <: C rd u {x} if x is a shared capability.We can map regular capture sets to read-only sets:
C _ <: ro(C) rdRead-only capabilities in regular capture sets can be widened to exclusive capabilities:
{x.rd, xs} _ <: {x, xs} _One case where an explicit capture set mode would be useful concerns refinements of type variable bounds, as in the following example.
class A:
type T <: Object^{x.rd, y}
class B extends A:
type T <: Object^{x.rd}
class C extends B:
type T = Matrix^{x.rd}
We assume that x and y are exclusive capabilities.
The capture set of type T in class C is a read-only set since Matrix extends Mutable. But the capture sets of the occurrences of
T in A and B are regular. This leads to an error in bounds checking
the definition of T in C against the one in B
since read-only sets do not subcapture regular sets. We can fix the
problem by declaring the capture set in class B as read-only:
class B extends A:
type T <: Object^{x.rd}.rd
But now a different problem arises since the capture set of T in B is
read-only but the capture set of T and A is regular. The capture set of
T in A cannot be made read-only since it contains an exclusive capability y. So we'd have to drop y and declare class A like this:
class A:
type T <: Object^{x.rd}.rd
A read-only access is a reference x to a type extending Mutable with a regular capture set if the expected type is one of the following:
A read-only access contributes the read-only capability x.rd to its environment (as formalized by cv). Other accesses contribute the full capability x.
A reference p.m to an update method or class m of a mutable type is allowed only if p's capture set is regular.
If e is an expression of a type T^cs extending Mutable and the expected type is a value type that is not a mutable type, then the type of e is mapped to T^ro(cs).