From 90ae8f9fcdf956bed70cb19be80ed7e638fbdb5a 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 01/11] 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 fe4f394db59d45abea29d2328fce2714814c97d0 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 02/11] 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 47c5fa3956889641dafb64957dd1d890948a1115 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 03/11] 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 b898c4936b95c28593f148a55fda63d82948e4a2 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 04/11] 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 bf8de892615393caee60b54656c6210b113d9526 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Mon, 8 Dec 2025 17:42:09 +0100 Subject: [PATCH 05/11] Update polymorphism section in cc language ref --- .../capture-checking/polymorphism.md | 177 +++++++++++++----- 1 file changed, 132 insertions(+), 45 deletions(-) diff --git a/docs/_docs/reference/experimental/capture-checking/polymorphism.md b/docs/_docs/reference/experimental/capture-checking/polymorphism.md index 8853b54c82a2..5cfbccc37958 100644 --- a/docs/_docs/reference/experimental/capture-checking/polymorphism.md +++ b/docs/_docs/reference/experimental/capture-checking/polymorphism.md @@ -6,8 +6,44 @@ nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-che ## Introduction -It is sometimes convenient to write operations that are parameterized with a capture set of capabilities. For instance consider a type of event sources -`Source` on which `Listener`s can be registered. Listeners can hold certain capabilities, which show up as a parameter to `Source`: +Capture checking supports capture-polymorphic programming in two complementary styles: + 1. **Implicit** capture polymorphism, which is the default and has minimal syntactic overhead. + 2. **Explicit** capture polymorphism, which allows programmers to abstract over capture sets directly through explicit generic parameters. + +### Implicit Polymorphism + +In many cases, such a higher-order functions, we do not need new syntax to be polymorphic over +capturing types. The classic example is `map` over lists: +```scala +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` +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 +[capture tunneling](classes.md#capture-tunneling) mechanism for generic types, we get effect +polymorphism _for free_, and no signature changes are necessary on an eager collection type +such as `List`. + +Contrasting this against lazy collections such as `LzyList` from the [previous section](classes.md), +the implicit capability polymorphism induces an additional capture set on the result of `map`: +```scala +extension [A](xs: LzyList[A]^) + def map[B](f: A => B): LzyList[B]^{xs, f} +``` +Unlike the eager version which only uses `f` during the computation, the lazy counterpart delays the +computation, so that the original list and the function are captured by the result. +This relationship can be succinctly expressed due to the path-dependent result capture set +`{xs, f}` and would be rather cumbersome to express in more traditional effect-type systems +with explicit generic effect parameters. + +### Explicit Polymorphism + +In some situations, it is convenient or necessary to parameterize definitions by a capture set. +This allows an API to state precisely which capabilities its clients may use. Consider a `Source` +that stores `Listeners`: ```scala class Source[X^]: private var listeners: Set[Listener^{X}] = Set.empty @@ -16,77 +52,128 @@ class Source[X^]: def allListeners: Set[Listener^{X}] = listeners ``` -The type variable `X^` can be instantiated with a set of capabilities. It can occur in capture sets in its scope. For instance, in the example above -we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X`. The `register` method takes a listener of this type -and assigns it to the variable. +Here, `X^` is a _capture-set variable_. It may appear inside capture sets throughout the class body. +The field listeners holds exactly the listeners that capture X, and register only accepts such +listeners. Capture-set variables `X^` without user-annotated bounds by default range over the interval `>: {} <: {caps.cap}` which is the universe of capture sets instead of regular types. -Under the hood, such capture-set variables are represented as regular type variables within the special interval - `>: CapSet <: CapSet^`. -For instance, `Source` from above could be equivalently -defined as follows: +#### 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 + 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: ```scala class Source[X >: CapSet <: CapSet^]: ... ``` -`CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only -purpose is to identify type variables which are capture sets. In non-capture-checked -usage contexts, the type system will treat `CapSet^{a}` and `CapSet^{a,b}` as the type `CapSet`, whereas -with capture checking enabled, it will take the annotated capture sets into account, -so that `CapSet^{a}` and `CapSet^{a,b}` are distinct. -This representation based on `CapSet` is subject to change and -its direct use is discouraged. - -Capture-set variables can be inferred like regular type variables. When they should be instantiated -explicitly one supplies a concrete capture set. For instance: +`CapSet` is a sealed marker trait in `caps` used internally to distinguish capture-set variables. +It cannot be instantiated or extended; in non–capture-checked code, `CapSet^{a}` and `CapSet^{a,b}` +erase to plain `CapSet`, while with capture checking enabled their capture sets remain distinct. +This representation is an implementation detail and should not be used directly. + +#### Instantiation and inference +Capture-set variables are inferred in the same way as ordinary type variables. +They can also be instantiated explicitly: ```scala class Async extends caps.SharedCapability -def listener(async: Async): Listener^{async} = ??? +def listener(a: Async): Listener^{a} = ??? -def test1(async1: Async, others: List[Async]) = - val src = Source[{async1, others*}] - ... -``` -Here, `src` is created as a `Source` on which listeners can be registered that refer to the `async` capability or to any of the capabilities in list `others`. So we can continue the example code above as follows: -```scala +def test1[X^](async1: Async, others: List[Async^{X}]) = + val src = Source[{async1, X}] src.register(listener(async1)) others.map(listener).foreach(src.register) - val ls: Set[Listener^{async, others*}] = src.allListeners + val ls: Set[Listener^{async1, X}] = src.allListeners +``` +Here, `src` accepts listeners that may capture either the specific capability `async1` or any element of +others. The resulting `allListeners` method reflects this relationship. + +#### Transforming collections +A typical use of explicit capture parameters arises when transforming collections of capturing +values—such as `Future`s. In these cases, the API must guarantee that whatever capabilities are +captured by the elements of the input collection are also captured by the elements of the output. + +The following example takes an unordered `Set` of futures and produces a `Stream` that yields their +results in the order in which the futures complete. Using an explicit capture variable `C^`, the +signature expresses that the cumulative capture set of the input futures is preserved in the +resulting stream: +```scala +def collect[T, C^](fs: Set[Future[T]]^{C})(using Async^): Stream[Future[T]^{C}] = + val channel = Channel() + fs.forEach.(_.onComplete(v => channel.send(v))) + Stream.of(channel) ``` -A common use-case for explicit capture parameters is describing changes to the captures of mutable fields, such as concatenating -effectful iterators: + +#### Tracking the evolution of mutable objects +A common use case for explicit capture parameters is when a mutable object’s reachable capabilities +_grow_ due to mutation. For example, concatenating effectful iterators: ```scala class ConcatIterator[A, C^](var iterators: mutable.List[IterableOnce[A]^{C}]): def concat(it: IterableOnce[A]^): ConcatIterator[A, {C, it}]^{this, it} = iterators ++= it // ^ this // track contents of `it` in the result ``` -In such a scenario, we also should ensure that any pre-existing alias of a `ConcatIterator` object should become -inaccessible after invoking its `concat` method. This is achieved with [mutation and separation tracking](separation-checking.md) which are currently in development. +In such cases, the type system must ensure that any existing aliases of the iterator become invalid +after mutation. This is handled by [mutation tracking](mutability.md) and [separation tracking](separation-checking.md), which are currently under development. + +## Shall I Be Implicit or Explicit? + +Implicit capability polymorphism is intended to cover the most common use cases. +It integrates smoothly with existing functional programming idioms and was expressive enough to +retrofit the Scala standard collections library to capture checking with minimal changes. + +Explicit capability polymorphism is introduced only when the capture relationships of an API must be +stated directly in its signature. At this point, we have seen several examples where doing so improves +clarity: naming a capture set explicitly, preserving the captures of a collection, or describing how +mutation changes the captures of an object. + +The drawback of explicit polymorphism is additional syntactic overhead. Capture parameters can make +signatures more verbose, especially in APIs that combine several related capture sets. + +**Recommendation:** Prefer implicit polymorphism by default. +Introduce explicit capture parameters only when the intended capture relationships cannot be expressed +implicitly or would otherwise be unclear. ## Capability Members -Just as parametrization by types can be equally expressed with type members, we could -also define the `Source[X^]` class above using a _capability member_: +Capture parameters can also be introduced as *capability members*, in the same way that type +parameters can be replaced with type members. The earlier example +```scala +class Source[X^]: + private var listeners: Set[Listener^{X}] = Set.empty +``` +can be written instead as: ```scala class Source: type X^ private var listeners: Set[Listener^{this.X}] = Set.empty - ... // as before + + def register(l: Listener^{this.X]): Unit = + listeners += l + + def allListeners: Set[Listener^{this.X}] = listeners ``` -Here, we can refer to capability members using paths in capture sets (such as `{this.X}`). Similarly to type members, -capability members can be upper- and lower-bounded with capture sets: -```scala -trait Thread: - type Cap^ - def run(block: () ->{this.Cap} -> Unit): Unit +A capability member behaves like a path-dependent capture-set variable. It may appear in capture +annotations using paths such as `{this.X}`. -trait GPUThread extends Thread: - type Cap^ >: {cudaMalloc, cudaFree} <: {caps.cap} +Capability members can also have capture-set bounds, restricting which capabilities they may contain: +```scala +trait Reactor: + type Cap^ <: {caps.cap} + def onEvent(h: Event ->{this.Cap} Unit): Unit +``` +Each implementation of Reactor may refine `Cap^` to a more specific capture set: +```scala +trait GUIReactor extends Reactor: + type Cap^ <: {ui, log} ``` -Since `caps.cap` is the top element for subcapturing, we could have also left out the -upper bound: `type Cap^ >: {cudaMalloc, cudaFree}`. +Here, `GUIReactor` specifies that event handlers may capture only `ui`, `log`, or a subset thereof. +The `onEvent` method expresses this via the path-dependent capture set `{this.Cap}`. + +Capability members are useful when capture information should be tied to object identity or form part +of an abstract interface, instead of being expressed through explicit capture parameters. -**Advanced uses:** We discuss more advanced uses cases for capability members [here](advanced.md). +**Advanced uses:** We discuss more advanced use cases for capability members [here](advanced.md). From d73dd15a87c9d08b529a23f1afce46716d1abcb2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Mon, 8 Dec 2025 17:47:47 +0100 Subject: [PATCH 06/11] Nits --- .../experimental/capture-checking/polymorphism.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/docs/_docs/reference/experimental/capture-checking/polymorphism.md b/docs/_docs/reference/experimental/capture-checking/polymorphism.md index 5cfbccc37958..a971cc30f4e4 100644 --- a/docs/_docs/reference/experimental/capture-checking/polymorphism.md +++ b/docs/_docs/reference/experimental/capture-checking/polymorphism.md @@ -7,8 +7,9 @@ nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-che ## Introduction Capture checking supports capture-polymorphic programming in two complementary styles: - 1. **Implicit** capture polymorphism, which is the default and has minimal syntactic overhead. - 2. **Explicit** capture polymorphism, which allows programmers to abstract over capture sets directly through explicit generic parameters. + +1. **Implicit** capture polymorphism, which is the default and has minimal syntactic overhead. +1. **Explicit** capture polymorphism, which allows programmers to abstract over capture sets directly through explicit generic parameters. ### Implicit Polymorphism @@ -117,7 +118,7 @@ class ConcatIterator[A, C^](var iterators: mutable.List[IterableOnce[A]^{C}]): this // track contents of `it` in the result ``` In such cases, the type system must ensure that any existing aliases of the iterator become invalid -after mutation. This is handled by [mutation tracking](mutability.md) and [separation tracking](separation-checking.md), which are currently under development. +after mutation. This is handled by [mutation tracking](mutability.md) and [separation tracking](separation-checking.md), which are currently under development. ## Shall I Be Implicit or Explicit? From b07e36cf7830cd89ab46155e366239334b3d86b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Tue, 9 Dec 2025 16:57:04 +0100 Subject: [PATCH 07/11] Pass over scoped-caps --- .../capture-checking/scoped-caps.md | 219 +++++++++++++----- 1 file changed, 155 insertions(+), 64 deletions(-) diff --git a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md index b0296fb47b03..0ca4afbccdd5 100644 --- a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md +++ b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md @@ -6,55 +6,59 @@ nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-che ## Scoped Universal Capabilities -When discussing escape checking, we referred to a scoping discipline. That is, capture sets can contain only capabilities that are visible at the point where the set is defined. But that raises the question where a universal capability `cap` is defined? In fact, what is written as the top type `cap` can mean different capabilities, depending on scope. Usually a `cap` refers to a universal capability defined in the scope where the `cap` appears. +When discussing escape checking, we referred to a scoping discipline. That is, capture sets can contain only capabilities that are visible at the point where the set is defined. But that raises the question: where is a universal capability `cap` defined? In fact, what is written as the top type `cap` can mean different capabilities, depending on scope. Usually a `cap` refers to a universal capability defined in the scope where the `cap` appears. + +### Existential Binding Special rules apply to `cap`s in method and function parameters and results. For example, take this method: ```scala - def makeLogger(fs: FileSystem^): Logger^ = new Logger(fs) +def makeLogger(fs: FileSystem^): Logger^ = new Logger(fs) ``` -This creates a `Logger` that captures `fs`. -We could have been more specific in specifying `Logger^{fs}` as the return type of makeLogger, but the current definition is also valid, and might be preferable if we want to hide details what the returned logger captures. If we write it as above then certainly the implied `cap` in the return type of `Logger` should be able subsume the capability `fs`. This means that this `cap` has to be defined in a scope in which -`fs` is visible. + +This creates a `Logger` that captures `fs`. We could have been more specific in specifying `Logger^{fs}` as the return type, but the current definition is also valid, and might be preferable if we want to hide details of what the returned logger captures. If we write it as above then certainly the implied `cap` in the return type should be able to subsume the capability `fs`. This means that this `cap` has to be defined in a scope in which `fs` is visible. In logic, the usual way to achieve this scoping is with an existential binder. We can express the type of `makeLogger` like this: ```scala makeLogger: (fs: ∃cap₁.FileSystem^{cap₁}): ∃cap₂. Logger^{cap₂} ``` -In words: `makeLogger` takes a parameter `fs` of type `Filesystem` capturing _some_ universal capability `cap` and returns a `Logger` capturing some other (possibly different) universal `cap`. +In words: `makeLogger` takes a parameter `fs` of type `Filesystem` capturing _some_ universal capability `cap₁` and returns a `Logger` capturing some other (possibly different) universal `cap₂`. -We can also turn the existential in the function parameter to a universal "forall" -in the function itself. In that alternative notation, the type of makeLogger would read like this: +We can also turn the existential in the function parameter to a universal "forall" in the function itself. In that alternative notation, the type of makeLogger would read like this: ```scala makeLogger: ∀cap₁.(fs: FileSystem^{cap₁}): ∃cap₂. Logger^{cap₂} ``` -There's a connection with [capture polymorphism](polymorphism.md) here. `cap`s in function parameters behave like additional -capture parameters that can be instantiated at the call site to arbitrary capabilities. +There's a connection with [capture polymorphism](polymorphism.md) here. `cap`s in function parameters behave like additional capture parameters that can be instantiated at the call site to arbitrary capabilities. + +### Function Types The conventions for method types carry over to function types. A function type ```scala - (x: T) -> U^ +(x: T) -> U^ ``` -is interpreted as having an existentially bound `cap` in the result, like this +is interpreted as having an existentially bound `cap` in the result, like this: ```scala - (x: T) -> ∃cap.U^{cap} +(x: T) -> ∃cap.U^{cap} ``` -The same rules hold for the other kinds of function arrows, `=>`, `?->`, and `?=>`. So `cap` can in this case -subsume the function parameter `x` since it is locally bound in the function result. +The same rules hold for the other kinds of function arrows, `=>`, `?->`, and `?=>`. So `cap` can in this case subsume the function parameter `x` since it is locally bound in the function result. -However, the expansion of `cap` into an existentially bound variable only applies to functions that use -the dependent function style syntax, with explicitly named parameters. Parametric functions such as -`A => B^` or `(A₍, ..., Aₖ) -> B^` don't bind their result cap in an existential quantifier. -For instance, the function +However, the expansion of `cap` into an existentially bound variable only applies to functions that use the dependent function style syntax, with explicitly named parameters. Parametric functions such as `A => B^` or `(A₁, ..., Aₖ) -> B^` don't bind their result cap in an existential quantifier. For instance, the function ```scala - (x: A) -> B -> C^ +(x: A) -> B -> C^ ``` is interpreted as ```scala - (x: A) -> ∃cap.B -> C^{cap} +(x: A) -> ∃cap.B -> C^{cap} ``` In other words, existential quantifiers are only inserted in results of function arrows that follow an explicitly named parameter list. +**Examples:** + + - `A => B` is an alias type that expands to `A ->{cap} B`, therefore + `(x: T) -> A => B` expands to `(x: T) -> ∃cap.(A ->{cap} B)`. + + - `(x: T) -> Iterator[A => B]` expands to `(x: T) -> ∃cap.Iterator[A ->{cap} B]` + To summarize: - If a function result type follows a named parameter list and contains covariant occurrences of `cap`, @@ -65,58 +69,145 @@ To summarize: - Occurrences of `cap` elsewhere are not translated. They can be seen as representing an existential in the scope of the definition in which they appear. -**Examples:** +### Fresh Capabilities vs Result Capabilities - - `A => B` is an alias type that expands to `A ->{cap} B`, therefore - `(x: T) -> A => B` expands to `(x: T) -> ∃cap.(A ->{cap} B)`. +Internally, the compiler represents scoped `cap` instances using two different mechanisms: + +- **Fresh capabilities** are used for most `cap` instances. They track a _hidden set_ of concrete capabilities they subsume. When you pass a `FileSystem^` to a function expecting `T^`, the fresh capability in the parameter learns that it subsumes your specific `FileSystem`. Fresh capabilities participate in subcapturing: if `{fs} <: {cap}`, the fresh capability records `fs` in its hidden set. + +- **Result capabilities** are used for `cap` in dependent function results. They are _rigid_—they don't accumulate a hidden set. Instead, two result capabilities can only be related through _unification_, which makes them equivalent. This prevents the result's capture set from being "polluted" by unrelated capabilities. + +The distinction matters when checking function subtyping: + +```scala +val f: (x: FileSystem^) -> Logger^ = ??? +val g: (x: FileSystem^) -> Logger^{x} = f // OK +``` + +Here, the result `cap` in `f`'s type is a result capability. When checking if `f` can be assigned to `g`, the checker unifies `f`'s result capability with `{x}`. This works because unification is symmetric—we're just saying "these represent the same capability." + +In contrast: + +```scala +val leaky: Logger^ = ??? +val f: (x: FileSystem^) -> Logger^ = x => leaky // Error +``` + +This fails because `leaky`'s capture set cannot flow into the result capability—result capabilities don't accept arbitrary capabilities through subsumption, only through unification with other result capabilities tied to the same function. + +## Levels and Escape Prevention + +Each capability has a _level_ corresponding to where it was defined. A capability can only be captured by scopes at the same level or nested more deeply. + +### How Levels Are Computed + +A capability's level is determined by its _level owner_, which the compiler computes by walking up the ownership chain until reaching a symbol that represents a level boundary. Level boundaries are: +- **Classes** (but not inner non-static module classes) +- **Methods** (but not accessors or constructors) - - `(x: T) -> Iterator[A => B]` expands to `() -> ∃cap.Iterator[A ->{cap} B]` - +The key differences are: +- **What's tracked**: Rust tracks memory validity (preventing dangling pointers). Scala CC tracks capability usage (preventing unauthorized effects). +- **Explicit vs. implicit**: Rust lifetimes are often written explicitly (`&'a T`). Scala CC levels are computed automatically from the program structure. +- **Granularity**: Rust lifetimes can distinguish different fields of a struct. Scala CC levels are coarser, tied to method and class boundaries. - \ No newline at end of file + +The closure's capture set `{localLogger}` would need to be widened to fit the return type `() -> Unit`, but there's no visible capability that covers `localLogger` and fits in the empty set. This is an error. From da877164e25f808e1ba7a533e92358fff858eeef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Tue, 9 Dec 2025 18:29:10 +0100 Subject: [PATCH 08/11] Pass over scoped-caps --- .../capture-checking/scoped-caps.md | 105 +++++++----------- 1 file changed, 43 insertions(+), 62 deletions(-) diff --git a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md index 0ca4afbccdd5..61f7fe80f169 100644 --- a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md +++ b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md @@ -8,6 +8,8 @@ nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-che When discussing escape checking, we referred to a scoping discipline. That is, capture sets can contain only capabilities that are visible at the point where the set is defined. But that raises the question: where is a universal capability `cap` defined? In fact, what is written as the top type `cap` can mean different capabilities, depending on scope. Usually a `cap` refers to a universal capability defined in the scope where the `cap` appears. +A useful mental model is to think of `cap` as a "container" that can _absorb_ concrete capabilities. When you write `T^` (shorthand for `T^{cap}`), you're saying "this value may capture some capabilities that will flow into this `cap`." Different `cap` instances in different scopes are different containers: a capability that flows into one doesn't automatically flow into another. + ### Existential Binding Special rules apply to `cap`s in method and function parameters and results. For example, take this method: @@ -16,7 +18,7 @@ Special rules apply to `cap`s in method and function parameters and results. For def makeLogger(fs: FileSystem^): Logger^ = new Logger(fs) ``` -This creates a `Logger` that captures `fs`. We could have been more specific in specifying `Logger^{fs}` as the return type, but the current definition is also valid, and might be preferable if we want to hide details of what the returned logger captures. If we write it as above then certainly the implied `cap` in the return type should be able to subsume the capability `fs`. This means that this `cap` has to be defined in a scope in which `fs` is visible. +This creates a `Logger` that captures `fs`. We could have been more specific in specifying `Logger^{fs}` as the return type, but the current definition is also valid, and might be preferable if we want to hide details of what the returned logger captures. If we write it as above then certainly the implied `cap` in the return type should be able to absorb the capability `fs`. This means that this `cap` has to be defined in a scope in which `fs` is visible. In logic, the usual way to achieve this scoping is with an existential binder. We can express the type of `makeLogger` like this: ```scala @@ -32,7 +34,7 @@ There's a connection with [capture polymorphism](polymorphism.md) here. `cap`s i ### Function Types -The conventions for method types carry over to function types. A function type +The conventions for method types carry over to function types. A dependent function type ```scala (x: T) -> U^ ``` @@ -40,7 +42,7 @@ is interpreted as having an existentially bound `cap` in the result, like this: ```scala (x: T) -> ∃cap.U^{cap} ``` -The same rules hold for the other kinds of function arrows, `=>`, `?->`, and `?=>`. So `cap` can in this case subsume the function parameter `x` since it is locally bound in the function result. +The same rules hold for the other kinds of function arrows, `=>`, `?->`, and `?=>`. So `cap` can in this case absorb the function parameter `x` since `x` is locally bound in the function result. However, the expansion of `cap` into an existentially bound variable only applies to functions that use the dependent function style syntax, with explicitly named parameters. Parametric functions such as `A => B^` or `(A₁, ..., Aₖ) -> B^` don't bind their result cap in an existential quantifier. For instance, the function ```scala @@ -54,10 +56,11 @@ In other words, existential quantifiers are only inserted in results of function **Examples:** - - `A => B` is an alias type that expands to `A ->{cap} B`, therefore - `(x: T) -> A => B` expands to `(x: T) -> ∃cap.(A ->{cap} B)`. + - `A => B` is an alias type that expands to `A ->{cap} B`. + - Therefore + `(x: T) -> A => B` expands to `(x: T) -> ∃c.(A ->{c} B)`. - - `(x: T) -> Iterator[A => B]` expands to `(x: T) -> ∃cap.Iterator[A ->{cap} B]` + - `(x: T) -> Iterator[A => B]` expands to `(x: T) -> ∃c.Iterator[A ->{c} B]` To summarize: @@ -69,35 +72,10 @@ To summarize: - Occurrences of `cap` elsewhere are not translated. They can be seen as representing an existential in the scope of the definition in which they appear. -### Fresh Capabilities vs Result Capabilities - -Internally, the compiler represents scoped `cap` instances using two different mechanisms: - -- **Fresh capabilities** are used for most `cap` instances. They track a _hidden set_ of concrete capabilities they subsume. When you pass a `FileSystem^` to a function expecting `T^`, the fresh capability in the parameter learns that it subsumes your specific `FileSystem`. Fresh capabilities participate in subcapturing: if `{fs} <: {cap}`, the fresh capability records `fs` in its hidden set. - -- **Result capabilities** are used for `cap` in dependent function results. They are _rigid_—they don't accumulate a hidden set. Instead, two result capabilities can only be related through _unification_, which makes them equivalent. This prevents the result's capture set from being "polluted" by unrelated capabilities. - -The distinction matters when checking function subtyping: - -```scala -val f: (x: FileSystem^) -> Logger^ = ??? -val g: (x: FileSystem^) -> Logger^{x} = f // OK -``` - -Here, the result `cap` in `f`'s type is a result capability. When checking if `f` can be assigned to `g`, the checker unifies `f`'s result capability with `{x}`. This works because unification is symmetric—we're just saying "these represent the same capability." - -In contrast: - -```scala -val leaky: Logger^ = ??? -val f: (x: FileSystem^) -> Logger^ = x => leaky // Error -``` - -This fails because `leaky`'s capture set cannot flow into the result capability—result capabilities don't accept arbitrary capabilities through subsumption, only through unification with other result capabilities tied to the same function. - ## Levels and Escape Prevention -Each capability has a _level_ corresponding to where it was defined. A capability can only be captured by scopes at the same level or nested more deeply. +Each capability has a _level_ corresponding to where it was defined. The level determines where a capability can flow: it can flow into `cap`s at the same level or more deeply nested, but not outward to enclosing scopes. Later sections on [capability classifiers](classifiers.md) will add a controlled +escape mechanism. ### How Levels Are Computed @@ -115,7 +93,7 @@ def outer(c1: Cap^) = // level: outer def inner(c2: Cap^) = // level: inner val y = 2 // level: inner val f = () => c2.use() - ref.set(f) // Error: cap2 would escape its level + ref.set(f) // Error: c2 would escape its level class Local: // level: Local def method(c3: Cap^) = // level: method @@ -129,12 +107,12 @@ Local values like `x`, `y`, and `z` don't define their own levels. They inherit ### The Level Check -A capability can flow into a capture set only if the capture set's scope is _contained in_ the capability's level owner. In the example above, `ref.set(f)` fails because: -- `ref`'s type parameter was instantiated at `outer`'s level -- `f` captures `cap2`, which is at `inner`'s level -- `outer` is not contained in `inner`, so `cap2` cannot flow into `ref` +A capability can flow into a `cap` only if that `cap`'s scope is _contained in_ the capability's level owner. In the example above, `ref.set(f)` fails because: +- `ref`'s type parameter has a `cap` that was instantiated at `outer`'s level +- `f` captures `c2`, which is at `inner`'s level +- `outer` is not contained in `inner`, so `c2` cannot flow into `ref`'s `cap` -This ensures capabilities can only flow "inward" to more nested scopes, never "outward" to enclosing ones. +This ensures capabilities flow "inward" to more nested scopes, never "outward" to enclosing ones. ### Comparison with Rust Lifetimes @@ -149,10 +127,13 @@ fn bad<'a>() -> &'a i32 { ``` ```scala -// Scala CC: rejected because cap would escape its level -def bad(): () -> Unit = - val cap = CC() - () => cap.use() +// Scala CC: rejected because c escapes inner's level to outer's level +def outer() = + var escape: () => Unit = () => () + def inner(c: Cap^) = + escape = () => c.use() // Error: c at inner's level cannot escape to outer + inner(Cap()) + escape ``` The key analogies are: @@ -162,47 +143,47 @@ The key analogies are: The key differences are: - **What's tracked**: Rust tracks memory validity (preventing dangling pointers). Scala CC tracks capability usage (preventing unauthorized effects). -- **Explicit vs. implicit**: Rust lifetimes are often written explicitly (`&'a T`). Scala CC levels are computed automatically from the program structure. -- **Granularity**: Rust lifetimes can distinguish different fields of a struct. Scala CC levels are coarser, tied to method and class boundaries. +- **Explicit vs. implicit**: Rust lifetimes are often written explicitly (`&'a T`). Scala capture checking levels are computed automatically from the program structure. ## Charging Captures to Enclosing Scopes -When a capability is used, the capture checker must verify that all enclosing scopes properly account for it. This process is called _charging_ the capability to the environment. +When a capability is used, it must flow into the `cap`s of all enclosing scopes. This process is +called _charging_ the capability to the environment. ```scala -def outer(cap1: FileSystem^): Unit = - def inner(): () ->{cap1} Unit = - () => cap1.read() // cap1 is used here +def outer(fs: FileSystem^): Unit = + def inner(): () ->{fs} Unit = + () => fs.read() // cap1 is used here inner() ``` -When the capture checker sees `cap1.read()`, it verifies that: -1. The immediately enclosing closure `() => cap1.read()` declares `cap1` in its capture set -2. The enclosing method `inner` accounts for `cap1` (it does, via its result type) -3. The enclosing method `outer` accounts for `cap1` (it does, via its parameter) +When the capture checker sees `fs.read()`, it verifies that `fs` can flow into each enclosing scope: +1. The immediately enclosing closure `() => fs.read()` must have `fs` in its capture set ✓ +2. The enclosing method `inner` must account for `fs` (it does, via its result type) ✓ +3. The enclosing method `outer` must account for `fs` (it does, via its parameter) ✓ -At each level, the checker verifies that the used capabilities are a _subcapture_ of what the scope declares: +If any scope refuses to absorb the capability, capture checking fails: ```scala def process(fs: FileSystem^): Unit = - val f: () -> Unit = () => fs.read() // Error: {fs} is not a subset of {} + val f: () -> Unit = () => fs.read() // Error: fs cannot flow into {} ``` -The closure is declared pure (`() -> Unit`), but uses `fs`. Since `{fs}` is not a subset of the empty capture set, capture checking fails. +The closure is declared pure (`() -> Unit`), meaning its `cap` is the empty set. The capability `fs` cannot flow into an empty set, so this is rejected. ## Visibility and Widening -As capabilities are charged to outer scopes, they are _filtered_ to include only those visible at each level. When a local capability cannot appear in a type (because it's not visible), the capture set is _widened_ to the smallest visible superset: +When capabilities flow outward to enclosing scopes, they must remain visible. A local capability cannot appear in a type outside its defining scope. In such cases, the capture set is _widened_ to the smallest visible superset: ```scala -def test(fs: FileSystem^): Logger^ = +def test(fs: FileSystem^): Logger^{cap} = val localLogger = Logger(fs) - localLogger // Type is widened from Logger^{localLogger} to Logger^{fs} + localLogger // Type widens from Logger^{localLogger} to Logger^{fs} ``` -Here, `localLogger` cannot appear in the result type because it's a local variable. The capture set `{localLogger}` is widened to `{fs}`, which covers it (since `localLogger` captures `fs`) and is visible outside `test`. +Here, `localLogger` cannot appear in the result type because it's a local variable. The capture set `{localLogger}` widens to `{fs}`, which covers it (since `localLogger` captures `fs`) and is visible outside `test`. In effect, `fs` flows into the result's `cap` instead of `localLogger`. -However, widening cannot always succeed: +However, widening cannot always find a valid target: ```scala def test(fs: FileSystem^): () -> Unit = @@ -210,4 +191,4 @@ def test(fs: FileSystem^): () -> Unit = () => localLogger.log("hello") // Error: cannot widen to empty set ``` -The closure's capture set `{localLogger}` would need to be widened to fit the return type `() -> Unit`, but there's no visible capability that covers `localLogger` and fits in the empty set. This is an error. +The closure captures `localLogger`, but the return type `() -> Unit` has an empty capture set. There's no visible capability that covers `localLogger` and can flow into an empty set, so the checker rejects this code. From f0ed9b7d3af79922836bb1eb17fffa3f0457aaf7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Wed, 10 Dec 2025 13:02:45 +0100 Subject: [PATCH 09/11] Pass over scoped-caps --- .../experimental/capture-checking/scoped-caps.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md index 61f7fe80f169..ce438322b352 100644 --- a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md +++ b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md @@ -8,7 +8,7 @@ nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-che When discussing escape checking, we referred to a scoping discipline. That is, capture sets can contain only capabilities that are visible at the point where the set is defined. But that raises the question: where is a universal capability `cap` defined? In fact, what is written as the top type `cap` can mean different capabilities, depending on scope. Usually a `cap` refers to a universal capability defined in the scope where the `cap` appears. -A useful mental model is to think of `cap` as a "container" that can _absorb_ concrete capabilities. When you write `T^` (shorthand for `T^{cap}`), you're saying "this value may capture some capabilities that will flow into this `cap`." Different `cap` instances in different scopes are different containers: a capability that flows into one doesn't automatically flow into another. +A useful mental model is to think of `cap` as a "container" that can _absorb_ concrete capabilities. When you write `T^` (shorthand for `T^{cap}`), you're saying "this value may capture some capabilities that will flow into this `cap`." Different `cap` instances in different scopes are different containers: a capability that flows into one doesn't automatically flow into another. We will further expand on this idea later when discussing [separation checking](separation-checking.md). ### Existential Binding @@ -44,7 +44,7 @@ is interpreted as having an existentially bound `cap` in the result, like this: ``` The same rules hold for the other kinds of function arrows, `=>`, `?->`, and `?=>`. So `cap` can in this case absorb the function parameter `x` since `x` is locally bound in the function result. -However, the expansion of `cap` into an existentially bound variable only applies to functions that use the dependent function style syntax, with explicitly named parameters. Parametric functions such as `A => B^` or `(A₁, ..., Aₖ) -> B^` don't bind their result cap in an existential quantifier. For instance, the function +However, the expansion of `cap` into an existentially bound variable only applies to functions that use the dependent function style syntax, with explicitly named parameters. Parametric functions such as `A => B^` or `(A₁, ..., Aₖ) -> B^` don't bind the `cap` in their return types in an existential quantifier. For instance, the function ```scala (x: A) -> B -> C^ ``` @@ -74,8 +74,8 @@ To summarize: ## Levels and Escape Prevention -Each capability has a _level_ corresponding to where it was defined. The level determines where a capability can flow: it can flow into `cap`s at the same level or more deeply nested, but not outward to enclosing scopes. Later sections on [capability classifiers](classifiers.md) will add a controlled -escape mechanism. +Each capability has a _level_ corresponding to where it was defined. The level determines where a capability can flow: it can flow into `cap`s at the same level or more deeply nested, but not outward to enclosing scopes (which would mean a capability lives longer than its lexical lifetime). Later sections on [capability classifiers](classifiers.md) will add a controlled mechanism that permits escaping/flowing outward for situations +where this would be desirable. ### How Levels Are Computed @@ -153,7 +153,7 @@ called _charging_ the capability to the environment. ```scala def outer(fs: FileSystem^): Unit = def inner(): () ->{fs} Unit = - () => fs.read() // cap1 is used here + () => fs.read() // fs is used here inner() ``` @@ -173,10 +173,10 @@ The closure is declared pure (`() -> Unit`), meaning its `cap` is the empty set. ## Visibility and Widening -When capabilities flow outward to enclosing scopes, they must remain visible. A local capability cannot appear in a type outside its defining scope. In such cases, the capture set is _widened_ to the smallest visible superset: +When capabilities flow outward to enclosing scopes, they must remain visible. A local capability cannot appear in a type outside its defining scope. In such cases, the capture set is _widened_ to the smallest visible super capture set: ```scala -def test(fs: FileSystem^): Logger^{cap} = +def test(fs: FileSystem^): Logger^{fs} = val localLogger = Logger(fs) localLogger // Type widens from Logger^{localLogger} to Logger^{fs} ``` From 937300f4da3beb362b28586e915bc9c85540e5a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Wed, 10 Dec 2025 17:53:52 +0100 Subject: [PATCH 10/11] Pass over scoped-caps --- .../capture-checking/scoped-caps.md | 77 +++++++++++-------- 1 file changed, 43 insertions(+), 34 deletions(-) diff --git a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md index ce438322b352..8010d831e1ee 100644 --- a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md +++ b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md @@ -44,7 +44,8 @@ is interpreted as having an existentially bound `cap` in the result, like this: ``` The same rules hold for the other kinds of function arrows, `=>`, `?->`, and `?=>`. So `cap` can in this case absorb the function parameter `x` since `x` is locally bound in the function result. -However, the expansion of `cap` into an existentially bound variable only applies to functions that use the dependent function style syntax, with explicitly named parameters. Parametric functions such as `A => B^` or `(A₁, ..., Aₖ) -> B^` don't bind the `cap` in their return types in an existential quantifier. For instance, the function +However, the expansion of `cap` into an existentially bound variable only applies to functions that use the dependent function style syntax, with explicitly named parameters. Parametric functions such as `A => B^` or +`(A₁, ..., Aₖ) -> B^` don't bind the `cap` in their return types in an existential quantifier. For instance, the function ```scala (x: A) -> B -> C^ ``` @@ -60,7 +61,7 @@ In other words, existential quantifiers are only inserted in results of function - Therefore `(x: T) -> A => B` expands to `(x: T) -> ∃c.(A ->{c} B)`. - - `(x: T) -> Iterator[A => B]` expands to `(x: T) -> ∃c.Iterator[A ->{c} B]` + - `(x: T) -> Iterator[A => B]` expands to `(x: T) -> ∃c.Iterator[A ->{c} B]`. To summarize: @@ -116,39 +117,57 @@ This ensures capabilities flow "inward" to more nested scopes, never "outward" t ### Comparison with Rust Lifetimes -Readers familiar with Rust may notice similarities to lifetime checking. Both systems prevent references from escaping their valid scope: +Readers familiar with Rust may notice similarities to lifetime checking. Both systems prevent +references from escaping their valid scope. In Rust, a reference type `&'a T` carries an explicit +lifetime parameter `'a`. In Scala's capture checking, the lifetime is folded into the capability +name itself: `T^{x}` says "a `T` capturing `x`," and `x`'s level implicitly determines how long this +reference is valid. A capture set then acts as an upper bound on the lifetimes of all the +capabilities it contains. + +Consider a `withFile` pattern that ensures a file handle doesn't escape: ```rust -// Rust: rejected because x doesn't live long enough -fn bad<'a>() -> &'a i32 { - let x = 42; - &x +// Rust: the closure receives a reference bounded by 'a +fn with_file<'a, R>(path: &str, f: impl FnOnce(&'a File) -> R) -> R { + let file = File::open(path).unwrap(); + f(&file) +} + +fn main() { + let escaped: &File; + with_file("test.txt", |file| { + escaped = file; // Error: borrowed value does not live long enough + }); } ``` ```scala -// Scala CC: rejected because c escapes inner's level to outer's level -def outer() = - var escape: () => Unit = () => () - def inner(c: Cap^) = - escape = () => c.use() // Error: c at inner's level cannot escape to outer - inner(Cap()) - escape +// Scala CC: the closure receives a capability whose level prevents escape +def withFile[R](path: String)(f: File^ => R): R = + val file = File.open(path) + f(file) + +def main() = + var escaped: File^ + withFile("test.txt"): file => + escaped = file // Error: file's level cannot escape to main's level ``` +In both cases, the type system prevents the handle from escaping the callback. Rust achieves this by requiring `'a` to be contained within the closure's scope. Scala achieves it by checking that `file`'s level (tied to `withFile`) cannot flow into `escaped`'s level (at `main`). + The key analogies are: -- **Levels ≈ Lifetimes**: Both represent "how long something is valid" -- **Containment ≈ Outlives**: Rust's `'a: 'b` (a outlives b) corresponds to Scala's level containment check (but inverted: inner scopes are contained in outer ones) -- **Escape prevention**: Both reject code where a reference/capability would outlive its scope +- **Capability name ≈ Lifetime parameter**: Where Rust writes `&'a T`, Scala writes `T^{x}`. The capability `x` carries its lifetime implicitly via its level. +- **Capture set ≈ Lifetime bound**: A capture set `{x, y}` bounds the lifetime of a value to be no longer than the shortest-lived capability it contains. +- **Level containment ≈ Outlives**: Rust's `'a: 'b` (a outlives b) corresponds to Scala's level check (inner scopes are contained in outer ones). The key differences are: - **What's tracked**: Rust tracks memory validity (preventing dangling pointers). Scala CC tracks capability usage (preventing unauthorized effects). -- **Explicit vs. implicit**: Rust lifetimes are often written explicitly (`&'a T`). Scala capture checking levels are computed automatically from the program structure. +- **Explicit vs. implicit**: Rust lifetimes are explicit parameters (`&'a T`). Scala levels are computed automatically from program structure: you name the capability, not the lifetime. ## Charging Captures to Enclosing Scopes -When a capability is used, it must flow into the `cap`s of all enclosing scopes. This process is -called _charging_ the capability to the environment. +When a capability is used, it must be checked for compatibility with the capture-set constraints of +all enclosing scopes. This process is called _charging_ the capability to the environment. ```scala def outer(fs: FileSystem^): Unit = @@ -158,7 +177,7 @@ def outer(fs: FileSystem^): Unit = ``` When the capture checker sees `fs.read()`, it verifies that `fs` can flow into each enclosing scope: -1. The immediately enclosing closure `() => fs.read()` must have `fs` in its capture set ✓ +1. The immediately enclosing closure `() => fs.read()` must permit `fs` in its capture set ✓ 2. The enclosing method `inner` must account for `fs` (it does, via its result type) ✓ 3. The enclosing method `outer` must account for `fs` (it does, via its parameter) ✓ @@ -171,24 +190,14 @@ def process(fs: FileSystem^): Unit = The closure is declared pure (`() -> Unit`), meaning its `cap` is the empty set. The capability `fs` cannot flow into an empty set, so this is rejected. -## Visibility and Widening +### Visibility and Widening When capabilities flow outward to enclosing scopes, they must remain visible. A local capability cannot appear in a type outside its defining scope. In such cases, the capture set is _widened_ to the smallest visible super capture set: ```scala -def test(fs: FileSystem^): Logger^{fs} = +def test(fs: FileSystem^): Logger^ = val localLogger = Logger(fs) localLogger // Type widens from Logger^{localLogger} to Logger^{fs} ``` -Here, `localLogger` cannot appear in the result type because it's a local variable. The capture set `{localLogger}` widens to `{fs}`, which covers it (since `localLogger` captures `fs`) and is visible outside `test`. In effect, `fs` flows into the result's `cap` instead of `localLogger`. - -However, widening cannot always find a valid target: - -```scala -def test(fs: FileSystem^): () -> Unit = - val localLogger = Logger(fs) - () => localLogger.log("hello") // Error: cannot widen to empty set -``` - -The closure captures `localLogger`, but the return type `() -> Unit` has an empty capture set. There's no visible capability that covers `localLogger` and can flow into an empty set, so the checker rejects this code. +Here, `localLogger` cannot appear in the result type because it's a local variable. The capture set `{localLogger}` widens to `{fs}`, which covers it (since `localLogger` captures `fs`) and is visible outside `test`. In effect, `fs` flows into the result's `cap` instead of `localLogger`. \ No newline at end of file From 494b0ac0cf86db2bd6c55b25d03dc3bc42193883 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Wed, 10 Dec 2025 18:12:34 +0100 Subject: [PATCH 11/11] Update scoped-caps --- .../experimental/capture-checking/scoped-caps.md | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md index 8010d831e1ee..ebcfb52cc325 100644 --- a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md +++ b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md @@ -89,12 +89,12 @@ Consider this example: ```scala def outer(c1: Cap^) = // level: outer val x = 1 // level: outer (vals don't create levels) - val ref = Ref[() => Unit](() => ()) + var ref: () => Unit = () => () def inner(c2: Cap^) = // level: inner val y = 2 // level: inner val f = () => c2.use() - ref.set(f) // Error: c2 would escape its level + ref = f // Error: c2 would escape its level class Local: // level: Local def method(c3: Cap^) = // level: method @@ -127,14 +127,18 @@ capabilities it contains. Consider a `withFile` pattern that ensures a file handle doesn't escape: ```rust +struct File; +impl File { fn open(_path: &str) -> Option { Some(File) } } + // Rust: the closure receives a reference bounded by 'a -fn with_file<'a, R>(path: &str, f: impl FnOnce(&'a File) -> R) -> R { +fn with_file(path: &str, f: impl for<'a> FnOnce(&'a File) -> R) -> R { let file = File::open(path).unwrap(); f(&file) } fn main() { - let escaped: &File; + let f = File; + let mut escaped: &File = &f; with_file("test.txt", |file| { escaped = file; // Error: borrowed value does not live long enough });