From 8f28e7bf70680a881d48f26ded0f5841fdc281bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Tue, 2 Dec 2025 18:06:34 +0100 Subject: [PATCH 1/5] CC docs: Add forward reference --- docs/_docs/reference/experimental/capture-checking/basics.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/_docs/reference/experimental/capture-checking/basics.md b/docs/_docs/reference/experimental/capture-checking/basics.md index 23924e97c8f6..4dba035f14bb 100644 --- a/docs/_docs/reference/experimental/capture-checking/basics.md +++ b/docs/_docs/reference/experimental/capture-checking/basics.md @@ -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: From 081ed0b537a48907ee610cdcfb0b9f92b770467b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Thu, 4 Dec 2025 12:37:14 +0100 Subject: [PATCH 2/5] Fix warnings during generateScalaDocumentation --- docs/_docs/contributing/scaladoc.md | 4 ++-- docs/_docs/reference/metaprogramming/reflection.md | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/_docs/contributing/scaladoc.md b/docs/_docs/contributing/scaladoc.md index 24161b63b4d2..34890617aea5 100644 --- a/docs/_docs/contributing/scaladoc.md +++ b/docs/_docs/contributing/scaladoc.md @@ -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. diff --git a/docs/_docs/reference/metaprogramming/reflection.md b/docs/_docs/reference/metaprogramming/reflection.md index 71f4555e6418..9275ec5d1bab 100644 --- a/docs/_docs/reference/metaprogramming/reflection.md +++ b/docs/_docs/reference/metaprogramming/reflection.md @@ -86,7 +86,7 @@ The above is represented in the quotes reflect API by a `Block` (a subtype of `T ``` You can see the whole hierarchy between different types of Trees in -[`reflectModule` documentation](https://scala-lang.org/api/3.3_LTS/scala/quoted/Quotes$reflectModule.html#`). +[`reflectModule` documentation](https://scala-lang.org/api/3.3_LTS/scala/quoted/Quotes$reflectModule.html). You can also check the shape of code by printing out quoted code transformed into a Term: ```scala From 425e79dd7fde86e45f4ce9c44fce7e530144d13a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Thu, 4 Dec 2025 13:11:25 +0100 Subject: [PATCH 3/5] Sync --- .../experimental/capture-checking/basics.md | 2 + .../experimental/capture-checking/classes.md | 41 ++++++++++++++++--- .../capture-checking/internals.md | 2 +- 3 files changed, 38 insertions(+), 7 deletions(-) diff --git a/docs/_docs/reference/experimental/capture-checking/basics.md b/docs/_docs/reference/experimental/capture-checking/basics.md index 4dba035f14bb..8d9df0d6b81e 100644 --- a/docs/_docs/reference/experimental/capture-checking/basics.md +++ b/docs/_docs/reference/experimental/capture-checking/basics.md @@ -347,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. diff --git a/docs/_docs/reference/experimental/capture-checking/classes.md b/docs/_docs/reference/experimental/capture-checking/classes.md index 9f9269915233..ec4c9082a92e 100644 --- a/docs/_docs/reference/experimental/capture-checking/classes.md +++ b/docs/_docs/reference/experimental/capture-checking/classes.md @@ -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} => ... @@ -73,7 +75,34 @@ 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 capabilities. + +For example: +```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 +``` + +## Capture Tunneling Consider the following simple definition of a `Pair` class: ```scala @@ -93,7 +122,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 @@ -144,7 +173,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. @@ -204,7 +233,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: @@ -218,7 +247,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: diff --git a/docs/_docs/reference/experimental/capture-checking/internals.md b/docs/_docs/reference/experimental/capture-checking/internals.md index 6aff9b208fd9..3a95ac0e25da 100644 --- a/docs/_docs/reference/experimental/capture-checking/internals.md +++ b/docs/_docs/reference/experimental/capture-checking/internals.md @@ -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 From e9e37776c686b672559a8a1ec167b6b8a770def7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Fri, 5 Dec 2025 16:30:57 +0100 Subject: [PATCH 4/5] Expand on this capture sets and inheritance --- docs/_docs/contributing/scaladoc.md | 2 +- .../experimental/capture-checking/classes.md | 37 ++++++++++++++++++- 2 files changed, 36 insertions(+), 3 deletions(-) diff --git a/docs/_docs/contributing/scaladoc.md b/docs/_docs/contributing/scaladoc.md index 34890617aea5..19660f036dbf 100644 --- a/docs/_docs/contributing/scaladoc.md +++ b/docs/_docs/contributing/scaladoc.md @@ -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 diff --git a/docs/_docs/reference/experimental/capture-checking/classes.md b/docs/_docs/reference/experimental/capture-checking/classes.md index ec4c9082a92e..d66b7437d101 100644 --- a/docs/_docs/reference/experimental/capture-checking/classes.md +++ b/docs/_docs/reference/experimental/capture-checking/classes.md @@ -77,9 +77,10 @@ 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 capabilities. +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: +For example (assuming all definitions are in the same file): ```scala class A: def fn: A = this // ok @@ -102,6 +103,38 @@ open class E: 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: From 99925fee027f12d05005fb79ca8762356e18169a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Mon, 15 Dec 2025 13:26:02 +0100 Subject: [PATCH 5/5] Address review comments --- docs/_docs/reference/experimental/capture-checking/classes.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/docs/_docs/reference/experimental/capture-checking/classes.md b/docs/_docs/reference/experimental/capture-checking/classes.md index d66b7437d101..792e03806b7b 100644 --- a/docs/_docs/reference/experimental/capture-checking/classes.md +++ b/docs/_docs/reference/experimental/capture-checking/classes.md @@ -77,9 +77,11 @@ 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 +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`). +¹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. + For example (assuming all definitions are in the same file): ```scala class A: