Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ of labels for lexically-delimited control operators:
trait Label extends Capability:
type Fv^ // the capability set occurring freely in the `block` passed to `boundary` below.

def boundary[T, C^](block: Label{type Fv = {C} } ->{C} T): T = ??? // ensure free caps of label and block match
def boundary[T, C^](block: Label{type Fv = {C} } ->{C} T): T = ??? // ensure free capabilities of label and block match
def suspend[U](label: Label)[D^ <: {label.Fv}](handler: () ->{D} U): U = ??? // may only capture the free capabilities of label

def test =
Expand Down
18 changes: 9 additions & 9 deletions docs/_docs/reference/experimental/capture-checking/basics.md
Original file line number Diff line number Diff line change
Expand Up @@ -96,8 +96,8 @@ must be a capturing type with a non-empty capture set. We also say that
variables that are capabilities are _tracked_.

In a sense, every
capability gets its authority from some other, more sweeping capability which it captures. The recursion stops with a _universal capability_, written `cap`, from which all other capabilities are ultimately derived.
If `T` is a type, then `T^` is a shorthand for `T^{cap}`, meaning `T` can capture arbitrary capabilities.
capability gets its authority from some other, more sweeping capability which it captures. The recursion stops with a _universal capability_, written `any`, from which all other capabilities are ultimately derived.
If `T` is a type, then `T^` is a shorthand for `T^{any}`, meaning `T` can capture arbitrary capabilities.

Here is an example:
```scala
Expand Down Expand Up @@ -139,7 +139,7 @@ One can add a capture set after the arrow of an otherwise pure function.
For instance, `A ->{c, d} B` would be a function that can capture capabilities `c` and `d`, but no others.
This type is a shorthand for `(A -> B)^{c, d}`, i.e. the function type `A -> B` with possible captures `{c, d}`.

The impure function type `A => B` is treated as an alias for `A ->{cap} B`. That is, impure functions are functions that can capture anything.
The impure function type `A => B` is treated as an alias for `A ->{any} B`. That is, impure functions are functions that can capture anything.

A capture annotation `^` binds more strongly than a function arrow. So
`A -> B^{c}` is read as `A -> (B^{c})` and `A -> B^` is read as `A -> (B^)`.
Expand Down Expand Up @@ -257,12 +257,12 @@ l : Logger^{fs}
```
we have
```
{l} <: {fs} <: {cap}
{fs} <: {fs, ct} <: {cap}
{ct} <: {fs, ct} <: {cap}
{l} <: {fs} <: {any}
{fs} <: {fs, ct} <: {any}
{ct} <: {fs, ct} <: {any}
```
The set consisting of the root capability `{cap}` covers every other capture set. This is
a consequence of the fact that, ultimately, every capability is created from `cap`.
The set consisting of the root capability `{any}` covers every other capture set. This is
a consequence of the fact that, ultimately, every capability is created from `any`.

**Example 2.** Consider again the FileSystem/Logger example from before. `LzyList[Int]` is a proper subtype of `LzyList[Int]^{l}`. So if the `test` method in that example
was declared with a result type `LzyList[Int]`, we'd get a type error. Here is the error message:
Expand All @@ -279,7 +279,7 @@ This widening is called _avoidance_; it is not specific to capture checking but

Classes like `CanThrow` or `FileSystem` have the property that their values are always intended to be capabilities. We can make this intention explicit and save boilerplate by letting these classes extend the `SharedCapability` class defined in object `caps`.

A type extending `SharedCapability` always comes with a capture set. If no capture set is given explicitly, we assume the capture set is `{cap}`.
A type extending `SharedCapability` always comes with a capture set. If no capture set is given explicitly, we assume the capture set is `{any}`.

This means we could equivalently express the `FileSystem` and `Logger` classes as follows:

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ Under the language import `language.experimental.captureChecking`, the code is i
```
14 | try () => xs.map(f).sum
| ^
|The expression's type () => Double is not allowed to capture the root capability `cap`.
|The expression's type () => Double is not allowed to capture the root capability `any`.
|This usually means that a capability persists longer than its allowed lifetime.
15 | catch case ex: LimitExceeded => () => -1
```
Expand Down
6 changes: 3 additions & 3 deletions docs/_docs/reference/experimental/capture-checking/classes.md
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ we know that the type of `this` must be pure, since `this` is the right hand sid
### Traits and Open Classes

The self-type inference behaves differently depending on whether all subclasses of a class are known. For a regular (non-open, non-abstract) class, all subclasses are known at compile time,¹ so the capture checker can precisely infer the self-type. However, for traits, abstract classes, and [`open`](../../other-new-features/open-classes.md) classes, arbitrary subclasses may exist, so the capture checker conservatively assumes that `this` may capture arbitrary capabilities
(i.e., it infers the universal capture set `cap`).
(i.e., it infers the universal capture set `any`).

¹We ignore here the possibility that non-open classes have subclasses in other compilation units (e.g. for testing) and assume that these subclasses do not change the inferred self type.

Expand Down Expand Up @@ -114,7 +114,7 @@ abstract class Root:
this: Root^ => // the default, can capture anything

abstract class Sub extends Root:
this: Sub^{a, b} => // ok, refinement {a, b} <: {cap}
this: Sub^{a, b} => // ok, refinement {a, b} <: {any}

class SubGood extends Sub:
val fld: AnyRef^{a} = a // ok, {a} included in {a, b}
Expand Down Expand Up @@ -337,7 +337,7 @@ Their capture annotations are all as one would expect:
- Concatenating two lazy lists produces a lazy list that captures both arguments.
- Dropping elements from a lazy list gives a safe approximation where the original list is captured in the result. In fact, it's only some suffix of the list that is retained at run time, but our modeling identifies lazy lists and their suffixes, so this additional knowledge would not be useful.

Of course the function passed to `map` or `filter` could also be pure. After all, `A -> B` is a subtype of `(A -> B)^{cap}` which is the same as `A => B`. In that case, the pure function
Of course the function passed to `map` or `filter` could also be pure. After all, `A -> B` is a subtype of `(A -> B)^{any}` which is the same as `A => B`. In that case, the pure function
argument will _not_ show up in the result type of `map` or `filter`. For instance:
```scala
val xs = squares(10)
Expand Down
18 changes: 9 additions & 9 deletions docs/_docs/reference/experimental/capture-checking/mutability.md
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,7 @@ of other objects. This property is expressed by extending the `Separate` trait i
```scala
trait Separate extends Stateful
```
If a value of a type extending Separate is created, a fresh `cap` is automatically
If a value of a type extending Separate is created, a fresh `any` is automatically
added to the value's capture set:
```scala
class S extends Separate
Expand Down Expand Up @@ -259,16 +259,16 @@ If `x` is an exclusive capability of a type extending `Stateful`, `x.rd` is its

**Implicitly added capture sets**

A reference to a type extending trait `Stateful` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given. This is different from other capability traits which implicitly add `{cap}`.
A reference to a type extending trait `Stateful` gets an implicit capture set `{any.rd}` provided no explicit capture set is given. This is different from other capability traits which implicitly add `{any}`.

For instance, consider:
```scala
def addContents(from: Ref[Int], to: Ref[Int]^): Unit =
to.set(to.get + from.get)
```
Here, `from` is implicitly read-only, and `to`'s type has capture set `cap`. I.e. with explicit capture sets this would read:
Here, `from` is implicitly read-only, and `to`'s type has capture set `any`. I.e. with explicit capture sets this would read:
```scala
def addContents(from: Ref[Int]^{cap.rd}, to: Ref[Int]^{cap}): Unit
def addContents(from: Ref[Int]^{any.rd}, to: Ref[Int]^{any}): Unit
```
In other words, the explicit `^` indicates where state changes can happen.

Expand All @@ -286,7 +286,7 @@ A _read-only access_ is a reference to a type extending `Stateful` where one of
```
2. The reference is a path where the path itself or a prefix of that path has a read-only capture set. For instance:
```scala
val r: Ref[Int]^{cap.rd} = new Ref[T](22)
val r: Ref[Int]^{any.rd} = new Ref[T](22)
def get = r.get // read-only access to `r`
```
Another example:
Expand All @@ -296,7 +296,7 @@ A _read-only access_ is a reference to a type extending `Stateful` where one of
val c: RefContainer = RefContainer()
def get = c.r.get // read-only access to `c.r`
```
In the last example, `c.r` is a read-only access since the prefix `c` is a read-only reference. Note that `^{cap.rd}` was implicitly added to `c: RefContainer` since `RefContainer` is a `Stateful` capability class.
In the last example, `c.r` is a read-only access since the prefix `c` is a read-only reference. Note that `^{any.rd}` was implicitly added to `c: RefContainer` since `RefContainer` is a `Stateful` capability class.
3. The expected type of the reference is a value type that is not a stateful type. For instance:
```scala
val r: Ref[Int]^ = Ref(22)
Expand Down Expand Up @@ -330,7 +330,7 @@ A reference to a stateful type with an exclusive capture set can be widened to a
```scala
val a: Ref[Int]^ = Ref(1)
val b1: Ref[Int]^{a.rd} = a
val b2: Ref[Int]^{cap.rd} = a
val b2: Ref[Int]^{any.rd} = a
```

## Lazy Vals and Read-Only Restrictions
Expand Down Expand Up @@ -428,13 +428,13 @@ The `untrackedCaptures` annotation can also be used in some other contexts unrel

## Read-Only Capsets

If we consider subtyping and subcapturing, we observe what looks like a contradiction: `x.rd` is seen as a restricted capability, so `{x.rd}` should subcapture `{x}`. Yet, we have seen in the example above that sometimes it goes the other way: `a`'s capture set is either `{a}` or `{cap}`, yet `a` can be used to define `b1` and `b2`, with capture sets `{a.rd}` and `{cap.rd}`, respectively.
If we consider subtyping and subcapturing, we observe what looks like a contradiction: `x.rd` is seen as a restricted capability, so `{x.rd}` should subcapture `{x}`. Yet, we have seen in the example above that sometimes it goes the other way: `a`'s capture set is either `{a}` or `{any}`, yet `a` can be used to define `b1` and `b2`, with capture sets `{a.rd}` and `{any.rd}`, respectively.

The contradiction can be explained by noting that we use a capture set in two different roles.

First, and as always, a capture set defines _retained capabilities_ that may or may be not used by a value. More capabilities give larger types, and the empty capture set is the smallest set according to that ordering. That makes sense: If a higher-order function like `map` is willing to accept a function `A => B` that can have arbitrary effects it's certainly OK to pass a pure function of type `A -> B` to it.

But for mutations, we use a capture set in a second role, in which it defines a set of _access permissions_. If we have a `Ref[T]^`, we can access all its methods, but if we have a `Ref[T]^{cap.rd}`, we can access only regular methods, not update methods. From that viewpoint a stateful type with exclusive capabilities lets you do more than a stateful type with just read-only capabilities. So by the Liskov substitution principle, sets with exclusive capabilities subcapture sets with only read-only capabilities.
But for mutations, we use a capture set in a second role, in which it defines a set of _access permissions_. If we have a `Ref[T]^`, we can access all its methods, but if we have a `Ref[T]^{any.rd}`, we can access only regular methods, not update methods. From that viewpoint a stateful type with exclusive capabilities lets you do more than a stateful type with just read-only capabilities. So by the Liskov substitution principle, sets with exclusive capabilities subcapture sets with only read-only capabilities.

The contradiction can be solved by distinguishing these two roles. For access permissions, we express read-only sets with an additional _qualifier_ `reader`. That qualifier is used only in the formal theory and the implementation, it currently cannot be expressed in source.
We add an implicit read-only qualifier `reader` to all capture sets on stateful types that consist only of shared or read-only capabilities.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ trait List[+A]:
// Works for pure functions AND capturing functions!
def map[B](f: A => B): List[B]
```
Due to the conventions established in previous sections, `f: A => B` translates to `f: A ->{cap} B`
Due to the conventions established in previous sections, `f: A => B` translates to `f: A ->{any} B`
under capture checking which means that the function argument `f` can capture any capability, i.e.,
`map` will have `f`'s effects, if we think of capabilities as the only means to induce side effects,
then _capability polymorphism equals effect polymorphism_. By careful choice of notation and the
Expand Down Expand Up @@ -63,7 +63,7 @@ listeners.
#### Under the hood

Capture-set variables without user-provided bounds range over the interval
`>: {} <: {caps.cap}` which is the full lattice of capture sets. They behave like type parameters
`>: {} <: {caps.any}` which is the full lattice of capture sets. They behave like type parameters
whose domain is "all capture sets", not all types.

Under the hood, a capture-set variable is implemented as a normal type parameter with special bounds:
Expand Down Expand Up @@ -166,7 +166,7 @@ annotations using paths such as `{this.X}`.
Capability members can also have capture-set bounds, restricting which capabilities they may contain:
```scala
trait Reactor:
type Cap^ <: {caps.cap}
type Cap^ <: {caps.any}
def onEvent(h: Event ->{this.Cap} Unit): Unit
```
Each implementation of Reactor may refine `Cap^` to a more specific capture set:
Expand Down
Loading
Loading