Skip to content
Draft
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
6 changes: 3 additions & 3 deletions docs/_docs/contributing/scaladoc.md
Original file line number Diff line number Diff line change
Expand Up @@ -74,8 +74,8 @@ You can also run specific signature tests with `testOnly`,
for example `scaladoc/testOnly *scaladoc.signatures.MarkdownCode`.

Most tests rely on comparing signatures (of classes, methods, objects etc.) extracted from the generated documentation
to signatures found in source files (extracted using Scalameta). Such tests are defined using [SignatureTest](test/dotty/tools/scaladoc/signatures/SignatureTest.scala) class
and its subtypes (such as [TranslatableSignaturesTestCases](test/dotty/tools/scaladoc/signatures/TranslatableSignaturesTestCases.scala)). In this style of test, it's not necessary for expected output to be included, because the test is its own specification.
to signatures found in source files (extracted using Scalameta). Such tests are defined using [SignatureTest](https://github.com/scala/scala3/blob/main/scaladoc/test/dotty/tools/scaladoc/signatures/SignatureTest.scala) class
and its subtypes (such as [TranslatableSignaturesTestCases](https://github.com/scala/scala3/blob/main/scaladoc/test/dotty/tools/scaladoc/signatures/TranslatableSignaturesTestCases.scala)). In this style of test, it's not necessary for expected output to be included, because the test is its own specification.

WARNING: As the classes mentioned above are likely to evolve, the description below might easily get out of date.
In case of any discrepancies rely on the source files instead.
Expand All @@ -84,7 +84,7 @@ In case of any discrepancies rely on the source files instead.
the names of directories containing corresponding TASTY files
and the kinds of signatures from source files (corresponding to keywords used to declare them like `def`, `class`, `object` etc.)
whose presence in the generated documentation will be checked (other signatures, when missing, will be ignored).
The mentioned source files should be located directly inside [](../scaladoc-testcases/src/tests) directory
The mentioned source files should be located directly inside the [scaladoc-testcases](https://github.com/scala/scala3/tree/main/scaladoc-testcases) directory
but the file names passed as parameters should contain neither this path prefix nor `.scala` suffix.

By default it's expected that all signatures from the source files will be present in the documentation
Expand Down
5 changes: 4 additions & 1 deletion docs/_docs/reference/experimental/capture-checking/basics.md
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,8 @@ val xs = usingLogFile { f =>
}
```
An error would be issued in the second case, but not the first one (this assumes a capture-aware
formulation `LzyList` of lazily evaluated lists, which we will present later in this page).
formulation `LzyList` of lazily evaluated lists, which we will present later in the chapter
on [capture checking classes](classes.md)).

It turns out that capture checking has very broad applications. Besides the various
try-with-resources patterns, it can also be a key part to the solutions of many other long standing problems in programming languages. Among them:
Expand Down Expand Up @@ -346,6 +347,8 @@ loophole()
But this will not compile either, since the capture set of the mutable variable `loophole` cannot refer to variable `f`, which is not visible
where `loophole` is defined.

### Monotonicity Rule

Looking at object graphs, we observe a monotonicity property: The capture set of an object `x` covers the capture sets of all objects reachable through `x`. This property is reflected in the type system by the following _monotonicity rule_:

- In a class `C` with a field `f`, the capture set `{this}` covers the capture set `{this.f}` as well as the capture set of any application of `this.f` to pure arguments.
74 changes: 68 additions & 6 deletions docs/_docs/reference/experimental/capture-checking/classes.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,9 @@ Here class `Super` has local capability `a`, which gets inherited by class
`Sub` and is combined with `Sub`'s own local capability `b`. Class `Sub` also has an argument capability corresponding to its parameter `x`. This capability gets instantiated to `c` in the final constructor call `Sub(c)`. Hence,
the capture set of that call is `{a, b, c}`.

The capture set of the type of `this` of a class is inferred by the capture checker, unless the type is explicitly declared with a self type annotation like this one:
## Capture Set of This

The capture set of the type of `this` of a class is inferred by the capture checker, unless the type is explicitly declared with a self-type annotation like this one:
```scala
class C:
self: D^{a, b} => ...
Expand Down Expand Up @@ -73,7 +75,67 @@ we know that the type of `this` must be pure, since `this` is the right hand sid
| of the enclosing class A
```

## Capture Tunnelling
### 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`).

For example (assuming all definitions are in the same file):
```scala
class A:
def fn: A = this // ok

trait B:
def fn: B = this // error
def fn2: B^ = this // ok

abstract class C:
def fn: C = this // error
def fn2: C^ = this // ok

sealed abstract class D:
def fn: D = this // ok

object D0 extends D

open class E:
def fn: E = this // error
def fn2: E^ = this // ok
```

### Inheritance

The capture set of `this` of a class or trait also serves as an upper bound of the possible capture
sets of extending classes
```scala
abstract class Root:
this: Root^ => // the default, can capture anything

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

class SubGood extends Sub:
val fld: AnyRef^{a} = a // ok, {a} included in {a, b}

class SubBad extends Sub:
val fld: IO^{io} = io // error, {io} not included in the this capture set {a, b}

class SubBad2 extends Sub:
this: SubBad2^{io} => // error, self type SubBad2^{e} does not conform to Sub^{c, d}
```

Generally, the further up a class hierarchy we go, the more permissive/impure the `this` capture set
of a class will be (and the more restrictive/pure it will be if we traverse the hierarchy downwards).
For example, Scala 3's top reference type `AnyRef`/`Object` conceptually has the universal
capability
```scala
class AnyRef:
this: AnyRef^ =>
// ...
```
Similarly, pure `Iterator`s are subtypes of impure ones.

## Capture Tunneling

Consider the following simple definition of a `Pair` class:
```scala
Expand All @@ -93,7 +155,7 @@ def p: Pair[Int ->{ct} String, Logger^{fs}] = Pair(x, y)
```
This might seem surprising. The `Pair(x, y)` value does capture capabilities `ct` and `fs`. Why don't they show up in its type at the outside?

The answer is capture tunnelling. Once a type variable is instantiated to a capturing type, the
The answer is capture tunneling. Once a type variable is instantiated to a capturing type, the
capture is not propagated beyond this point. On the other hand, if the type variable is instantiated
again on access, the capture information "pops out" again. For instance, even though `p` is technically pure because its capture set is empty, writing `p.fst` would record a reference to the captured capability `ct`. So if this access was put in a closure, the capability would again form part of the outer capture set. E.g.
```scala
Expand Down Expand Up @@ -144,7 +206,7 @@ end LzyCons
The `LzyCons` class takes two parameters: A head `hd` and a tail `tl`, which is a function
returning a `LzyList`. Both the function and its result can capture arbitrary capabilities.
The result of applying the function is memoized after the first dereference of `tail` in
the private mutable field `cache`. Note that the typing of the assignment `cache = tl()` relies on the monotonicity rule for `{this}` capture sets.
the private mutable field `cache`. Note that the typing of the assignment `cache = tl()` relies on the [monotonicity rule](basics.md#monotonicity-rule) for `{this}` capture sets.

Here is an extension method to define an infix cons operator `#:` for lazy lists. It is analogous
to `::` but instead of a strict list it produces a lazy list without evaluating its right operand.
Expand Down Expand Up @@ -204,7 +266,7 @@ Their capture annotations are all as one would expect:
- Filtering a lazy list produces a lazy list that captures the original list as well
as the (possibly impure) filtering predicate.
- 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 modelling identifies lazy lists and their suffixes, so this additional knowledge would not be useful.
- 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
argument will _not_ show up in the result type of `map` or `filter`. For instance:
Expand All @@ -218,7 +280,7 @@ argument does not show up since it is pure. Likewise, if the lazy list
This demonstrates that capability-based
effect systems with capture checking are naturally _effect polymorphic_.

This concludes our example. It's worth mentioning that an equivalent program defining and using standard, strict lists would require no capture annotations whatsoever. It would compile exactly as written now in standard Scala 3, yet one gets the capture checking for free. Essentially, `=>` already means "can capture anything" and since in a strict list side effecting operations are not retained in the result, there are no additional captures to record. A strict list could of course capture side-effecting closures in its elements but then tunnelling applies, since
This concludes our example. It's worth mentioning that an equivalent program defining and using standard, strict lists would require no capture annotations whatsoever. It would compile exactly as written now in standard Scala 3, yet one gets the capture checking for free. Essentially, `=>` already means "can capture anything" and since in a strict list side effecting operations are not retained in the result, there are no additional captures to record. A strict list could of course capture side-effecting closures in its elements but then tunneling applies, since
these elements are represented by a type variable. This means we don't need to annotate anything there either.

Another possibility would be a variant of lazy lists that requires all functions passed to `map`, `filter` and other operations like it to be pure. E.g. `map` on such a list would be defined like this:
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ that gets propagated and resolved further out.

When a mapping `m` is performed on a capture set variable `C`, a new variable `Cm` is created that contains the mapped elements and that is linked with `C`. If `C` subsequently acquires further elements through propagation, these are also propagated to `Cm` after being transformed by the `m` mapping. `Cm` also gets the same supersets as `C`, mapped again using `m`.

One interesting aspect of the capture checker concerns the implementation of capture tunnelling. The [foundational theory](https://infoscience.epfl.ch/record/290885) on which capture checking is based makes tunnelling explicit through so-called _box_ and
One interesting aspect of the capture checker concerns the implementation of capture tunneling. The [foundational theory](https://infoscience.epfl.ch/record/290885) on which capture checking is based makes tunneling explicit through so-called _box_ and
_unbox_ operations. Boxing hides a capture set and unboxing recovers it. The capture checker inserts virtual box and unbox operations based on actual and expected types similar to the way the type checker inserts implicit conversions. When capture set variables are first introduced, any capture set in a capturing type that is an instance of a type parameter instance is marked as "boxed". A boxing operation is
inserted if the expected type of an expression is a capturing type with
a boxed capture set variable. The effect of the insertion is that any references
Expand Down
Loading
Loading