diff --git a/docs/_docs/contributing/scaladoc.md b/docs/_docs/contributing/scaladoc.md index 24161b63b4d2..19660f036dbf 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. @@ -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/basics.md b/docs/_docs/reference/experimental/capture-checking/basics.md index 23924e97c8f6..8d9df0d6b81e 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: @@ -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. diff --git a/docs/_docs/reference/experimental/capture-checking/classes.md b/docs/_docs/reference/experimental/capture-checking/classes.md index 9f9269915233..d66b7437d101 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,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 @@ -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 @@ -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. @@ -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: @@ -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: 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 diff --git a/docs/_docs/reference/experimental/capture-checking/polymorphism.md b/docs/_docs/reference/experimental/capture-checking/polymorphism.md index 8853b54c82a2..a971cc30f4e4 100644 --- a/docs/_docs/reference/experimental/capture-checking/polymorphism.md +++ b/docs/_docs/reference/experimental/capture-checking/polymorphism.md @@ -6,8 +6,45 @@ 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. +1. **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 +53,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 ``` -A common use-case for explicit capture parameters is describing changes to the captures of mutable fields, such as concatenating -effectful iterators: +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) +``` + +#### 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). diff --git a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md index b0296fb47b03..ebcfb52cc325 100644 --- a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md +++ b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md @@ -6,55 +6,63 @@ 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. + +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 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 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 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. -The conventions for method types carry over to function types. A function type +### Function Types + +The conventions for method types carry over to function types. A dependent 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 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^ +(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) -> ∃c.(A ->{c} B)`. + + - `(x: T) -> Iterator[A => B]` expands to `(x: T) -> ∃c.Iterator[A ->{c} B]`. + To summarize: - If a function result type follows a named parameter list and contains covariant occurrences of `cap`, @@ -65,58 +73,135 @@ 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:** +## 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 (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 + +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) + +Consider this example: + +```scala +def outer(c1: Cap^) = // level: outer + val x = 1 // level: outer (vals don't create levels) + var ref: () => Unit = () => () + + def inner(c2: Cap^) = // level: inner + val y = 2 // level: inner + val f = () => c2.use() + ref = f // Error: c2 would escape its level + + class Local: // level: Local + def method(c3: Cap^) = // level: method + val z = c3 // level: method +``` + +Local values like `x`, `y`, and `z` don't define their own levels. They inherit the level of their enclosing method or class. This means: +- `c1` and `ref` are both at `outer`'s level +- `c2` and `f` are both at `inner`'s level +- `c3` and `z` are both at `method`'s level + +### The Level Check + +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` - - `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)`. +This ensures capabilities flow "inward" to more nested scopes, never "outward" to enclosing ones. - - `(x: T) -> Iterator[A => B]` expands to `() -> ∃cap.Iterator[A ->{cap} B]` - +Consider a `withFile` pattern that ensures a file handle doesn't escape: - \ No newline at end of file + +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 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