WIP add separation checking

odersky · odersky · commit 04a496bf2fbc · 2025-08-15T17:03:15.000+02:00
diff --git a/docs/_docs/internals/exclusive-capabilities.md b/docs/_docs/internals/exclusive-capabilities.md
@@ -6,21 +6,19 @@ Language design draft
 ## Capability Kinds
 
 A capability is called
-  - _exclusive_ if it is `cap` or it has an exclusive capability in its capture set.
-  - _shared_ otherwise.
-
-There is a new top capability `shared` which can be used as a capability for deriving shared capture sets. Other shared capabilities are created as read-only versions of exclusive capabilities.
+  - _shared_ if it is classified as a `SharedCapability`
+  - _exclusive_ otherwise.
 
 ## Update Methods
 
 We introduce a new trait
 ```scala
-trait Mutable
+trait Mutable extends ExclusiveCapability, Classifier
 ```
 It is used as a base trait for types that define _update methods_ using
 a new soft modifier `update`.
 
-`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are  defined locally or passed to it in parameters.
+`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined locally or passed to it in parameters.
 
 **Example:**
 ```scala
@@ -115,11 +113,6 @@ a method that accesses exclusive capabilities.
 
 If `x` is an exclusive capability of a type extending `Mutable`, `x.rd` is its associated, shared _read-only_ capability.
 
-`shared` can be understood as the read-only capability corresponding to `cap`.
-```scala
-  shared = cap.rd
-```
-
 A _top capability_ is either `cap` or `shared`.
 
 
@@ -134,7 +127,7 @@ The meaning of `^` and `=>` is the same as before:
 
 **Implicitly added capture sets**
 
-A reference to a type extending any of the traits `Capability` or `Mutable` gets an implicit capture set `{shared}` in case no explicit capture set is given.
+A reference to a type extending trait `Mutable` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given.
 
 For instance, a matrix multiplication method can be expressed as follows:
 
@@ -148,7 +141,7 @@ def mul(a: Matrix, b: Matrix, c: Matrix^): Unit =
 ```
 Here, `a` and `b` are implicitly read-only, and `c`'s type has capture set `cap`. I.e. with explicit capture sets this would read:
 ```scala
-def mul(a: Matrix^{shared}, b: Matrix^{shared}, c: Matrix^{cap}): Unit
+def mul(a: Matrix^{cap.rd}, b: Matrix^{cap.rd}, c: Matrix^{cap}): Unit
 ```
 Separation checking will then make sure that `a` and `b` must be different from `c`.
 
@@ -173,8 +166,6 @@ The read-only function `ro` maps capture sets to read-only capture sets. It is d
  - `ro(x)    =  x` if `x` is shared
  - `ro(x)    =  x.rd` if `x` is exclusive
 
-
-
 ## Subcapturing
 
 Subcapturing has to take the mode of capture sets into account. We let `m` stand for arbitrary modes.
@@ -271,7 +262,7 @@ A reference `p.m` to an update method or class `m` of a mutable type is allowed
 
 If `e` is an expression of a type `T^cs` extending `Mutable` and the expected type is a value type that is not a mutable type, then the type of `e` is mapped to `T^ro(cs)`.
 
-
+<!--
 ## Expression Typing
 
 An expression's type should never contain a top capability in its deep capture set. This is achieved by the following rules:
@@ -302,7 +293,6 @@ An expression's type should never contain a top capability in its deep capture s
    where the capture set of `x` contains a top capability,
    replace `x` by a fresh skolem `val sk: T`. Alternatively: keep it as is, but don't widen it.
 
-
 ## Post Processing Right Hand Sides
 
 The type of the right hand sides of `val`s or `def`s is post-processed before it becomes the inferred type or is compared with the declared type. Post processing
@@ -340,7 +330,7 @@ Since expression types can't mention cap, widening happens only
 
 **Definitions:**
 
- - The _transitive capture set_ `tcs(c)` of a capability `c` with underlying capture set `C` is `c` itself, plus the transitive capture set of `C`, but excluding `cap` or `shared`.
+ - The _transitive capture set_ `tcs(c)` of a capability `c` with underlying capture set `C` is `c` itself, plus the transitive capture set of `C`.
 
  - The _transitive capture set_ `tcs(C)` of a capture set C is the union
    of `tcs(c)` for all elements `c` of `C`.
@@ -356,7 +346,9 @@ Since expression types can't mention cap, widening happens only
 
 **Algorithm outline:**
 
- - Associate _shadowed sets_ with blocks, template statement sequences, applications, and val symbols. The idea is that a shadowed set gets populated when a capture reference is widened to cap. In that case the original references that were widened get added to the set.
+
+
+ Associate _shadowed sets_ with blocks, template statement sequences, applications, and val symbols. The idea is that a shadowed set gets populated when a capture reference is widened to cap. In that case the original references that were widened get added to the set.
 
  - After processing a `val x: T2 = t` with `t: T1` after post-processing:
 
diff --git a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md
@@ -4,7 +4,7 @@ title: "Scoped Caps"
 nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/scoped-caps.html
 ---
 
-## Introduction
+## 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.
 
@@ -84,6 +84,7 @@ To summarize:
   variable `ex` is replaced by `cap`.
 -->
 
+<!--
 ## Reach Capabilities
 
 Say you have a method `f` that takes an impure function argument which gets stored in a `var`:
@@ -118,3 +119,4 @@ def f(ops: List[A => B])
   ...
 ```
 Reach capabilities take the form `x*` where `x` is syntactically a regular capability. If `x: T` then `x*` stands for any capability that appears covariantly in `T` and that is accessed through `x`. The least supertype of this capability is the set of all capabilities appearing covariantly in `T`.
+-->
diff --git a/docs/_docs/reference/experimental/capture-checking/separation-checking.md b/docs/_docs/reference/experimental/capture-checking/separation-checking.md
@@ -4,4 +4,245 @@ title: "Separation Checking"
 nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/separation-checking.html
 ---
 
-## TODO
+## Introduction
+
+Separation checking is an extension of capture checking that enforces unique, un-aliased access to capabilities. It is enabled by a language import
+```scala
+import language.experimental.separationChecking
+```
+(or the corresponding setting `-language:experimental.separationChecking`).
+The import has to be given in addition to the `language.experimental.captureChecking` import that enables capture checking.
+The reason for the second language import is that separation checking is less mature than capture checking proper, so we are less sure
+we got the balance of safety and expressivity right for it at the present time.
+
+The purpose of separation checking is to ensure that certain accesses to capabilities are not aliased. As an example, consider matrix multiplication. A method that multiplies matrices `a`, and `b` into `c`,  could be declared like this:
+```scala
+def multiply(a: Matrix, b: Matrix, c: Matrix): Unit
+```
+But that signature alone does not tell us which matrices are supposed to be inputs and which one is the output. Nor does it guarantee that an input matrix is not re-used as the output, which would lead to wrong results.
+
+With separation checking, we can declare `Matrix` as a `Mutable` type, like this:
+```scala
+class Matrix(nrows: Int, ncols: Int) extends Mutable:
+  update def setElem(i: Int, j: Int, x: Double): Unit = ...
+  def getElem(i: Int, j: Int): Double = ...
+```
+We further declare that the `setElem` method in a `Matrix` is an `update` method, which means it has a side effect.
+
+Separation checking also gives a special interpretation to the following modified signature of `multiply`:
+```scala
+def multiply(a: Matrix, b: Matrix, c: Matrix^): Unit
+```
+In fact, only a single character was added: `c`'s type now carries a universal capability. This signature enforces at the same time two desirable properties:
+
+ - Matrices `a`, and `b` are read-only; `multiply` will not call their update method. By contrast, matrix `c` can be updated.
+ - Matrices `a` and `b` are different from matrix `c`, but `a` and `b` could refer to the same matrix.
+
+So, effectively, anything that can be updated must be unaliased.
+
+The idea behind separation checking is simple: We now interpret each occurrence of `cap` as a separate top capability. This includes derived syntaxes like `A^` and `B => C`. We further keep track during capture checking which capabilities are subsumed by each `cap`. If capture checking widens a capability `x` to the universal capability, we say `x` is _hidden_ by the universal. The rule then is that any capability hidden by a universal capability `capᵢ` cannot be referenced independently or hidden in another cap in code that can see `capᵢ`.
+
+Here's an example:
+```scala
+val x: C^ = y
+  ... x ...  // ok
+  ... y ...  // error
+```
+This principle ensures that capabilities such as `x` that have `cap` as underlying capture set are un-aliased or "fresh". Any previously existing aliases such as `y` in the code above are inaccessible as long as `x` is also visible.
+
+## Capability Kinds
+
+A capability is called
+  - _shared_ if it is [classified](../classifiers.md) as a `SharedCapability`
+  - _exclusive_ otherwise.
+
+## The Mutable Trait
+
+We introduce a new trait
+```scala
+trait Mutable extends ExclusiveCapability, Classifier
+```
+It is used as a [classifier](../classifiers.md) trait for types that define _update methods_ using
+a new soft modifier `update`.
+
+**Example:**
+```scala
+class Ref(init: Int) extends Mutable:
+  private var current = init
+  def get: Int = current
+  update def put(x: Int): Unit = current = x
+```
+`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined locally or passed to it in parameters.
+
+In class `Ref`, the `put` should be declared as an update method since it accesses the exclusive write capability of the variable `current` in its environment.
+
+`update` can also be used on an inner class of a class or object extending `Mutable`. It gives all code in the class the right
+to  access exclusive capabilities in the class environment. Normal classes
+can only access exclusive capabilities defined in the class or passed to it in parameters.
+
+```scala
+object Registry extends Mutable:
+  var count = 0
+  update class Counter:
+    update def next: Int =
+      count += 1
+      count
+```
+Normal method members of `Mutable` classes cannot call update methods. This is indicated since accesses in the callee are recorded in the caller. So if the callee captures exclusive capabilities so does the caller.
+
+An update method cannot implement or override a normal method, whereas normal methods may implement or override update methods. Since methods such as `toString` or `==` inherited from Object are normal methods, it follows that none of these methods may be implemented as an update method.
+
+The `apply` method of a function type is also a normal method, hence `Mutable` classes may not implement a function type with an update method as the `apply` method.
+
+## Mutable Types
+
+A type is called a _mutable_ if it extends `Mutable` and it has an update method or an update class as non-private member or constructor.
+
+When we create an instance of a mutable type we always add `cap` to its capture set. For instance, if class `Ref` is declared as shown previously then `new Ref(1)` has type `Ref[Int]^`.
+
+**Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type.
+
+**Definition:** A class is _read_only_ if the following conditions are met:
+
+ 1. It does not extend any exclusive capabilities from its environment.
+ 2. It does not take parameters with exclusive capabilities.
+ 3. It does not contain mutable fields, or fields that take exclusive capabilities.
+
+**Restriction:** If a class or trait extends `Mutable` all its parent classes or traits must either extend `Mutable` or be read-only.
+
+The idea is that when we upcast a reference to a type extending `Mutable` to a type that does not extend `Mutable`, we cannot possibly call a method on this reference that uses an exclusive capability. Indeed, by the previous restriction this class must be a read-only class, which means that none of the code implemented
+in the class can access exclusive capabilities on its own. And we
+also cannot override any of the methods of this class with a method
+accessing exclusive capabilities, since such a method would have
+to be an update method and update methods are not allowed to override regular methods.
+
+
+
+**Example:**
+
+Consider trait `IterableOnce` from the standard library.
+
+```scala
+trait IterableOnce[+T] extends Mutable:
+  def iterator: Iterator[T]^{this}
+  update def foreach(op: T => Unit): Unit
+  update def exists(op: T => Boolean): Boolean
+  ...
+```
+The trait is a mutable type with many update methods, among them `foreach` and `exists`. These need to be classified as `update` because their implementation in the subtrait `Iterator` uses the update method `next`.
+```scala
+trait Iterator[T] extends IterableOnce[T]:
+  def iterator = this
+  def hasNext: Boolean
+  update def next(): T
+  update def foreach(op: T => Unit): Unit = ...
+  update def exists(op; T => Boolean): Boolean = ...
+  ...
+```
+But there are other implementations of `IterableOnce` that are not mutable types (even though they do indirectly extend the `Mutable` trait). Notably, collection classes implement `IterableOnce` by creating a fresh
+`iterator` each time one is required. The mutation via `next()` is then restricted to the state of that iterator, whereas the underlying collection is unaffected. These implementations would implement each `update` method in `IterableOnce` by a normal method without the `update` modifier.
+
+```scala
+trait Iterable[T] extends IterableOnce[T]:
+  def iterator = new Iterator[T] { ... }
+  def foreach(op: T => Unit) = iterator.foreach(op)
+  def exists(op: T => Boolean) = iterator.exists(op)
+```
+Here, `Iterable` is not a mutable type since it has no update method as member.
+All inherited update methods are (re-)implemented by normal methods.
+
+**Note:** One might think that we don't need a base trait `Mutable` since in any case
+a mutable type is defined by the presence of update methods, not by what it extends. In fact the importance of `Mutable` is that it defines _the other methods_ as read-only methods that _cannot_ access exclusive capabilities. For types not extending `Mutable`, this is not the case. For instance, the `apply` method of a function type is not an update method and the type itself does not extend `Mutable`. But `apply` may well be implemented by
+a method that accesses exclusive capabilities.
+
+## Read-only Capabilities
+
+If `x` is an exclusive capability of a type extending `Mutable`, `x.rd` is its associated _read-only_ capability. It counts as a shared capability. A read-only capability does not permit access to the mutable fields of a matrix.
+
+A read-only capability can be seen as a classified capability
+using a classifier trait `Read` that extends `Mutable`. I.e.
+`x.rd` can be seen as being essentially the same as `x.only[Read]`.
+Currently, this precise equivalence is still waiting to be implemented.
+
+**Implicitly added capture sets**
+
+A reference to a type extending trait `Mutable` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given. This is different from
+other capability traits which implicitly add `{cap}`.
+
+For instance, consider the matrix multiplication method mentioned previously:
+```scala
+def multiply(a: Matrix, b: Matrix, c: Matrix^): Unit
+```
+It is expanded to
+```scala
+def multiply(a: Matrix^{cap.rd}, b: Matrix^{cap.rd}, c: Matrix^{cap}): Unit
+```
+Here, `a` and `b` are implicitly read-only, and `c`'s type has capture set `cap`. I.e. with explicit capture sets this would read:
+```scala
+def mul(a: Matrix^{cap.rd}, b: Matrix^{cap.rd}, c: Matrix^{cap}): Unit
+```
+Separation checking will then make sure that `a` and `b` must be different from `c`.
+
+## Accesses to Mutable Types
+
+An access `p.m` to an update method or class `m` in a mutable type is permitted only if the type of the prefix `M` retains exclusive capabilities. If `M` is pure or its capture set has only shared
+capabilities then the access is not permitted.
+
+A _read-only access_ is a reference `x` to a type extending `Mutable` that is either
+
+ - widened to a value type that is not a mutable type, or
+ - immediately followed by a selection with a member that is a normal method or class (not an update method or class).
+
+A read-only access charges the read-only capability `x.rd` to its environment. Other accesses charge the full capability `x`.
+
+**Example:**
+
+Consider a reference `x` and two closures `f` and `g`.
+
+```scala
+val x = Ref()
+val f = () => x.get    // f: () ->{x.rd} Unit
+val g = () => x.set(1) // g: () ->{x} Unit
+```
+
+`f` accesses a regular method, so it charges only `x.rd` to its environment which shows up in its capture set. Bu contrast, `g`
+accesses an update method of `x`,so its capture set is `{x}`.
+
+A reference to a mutable type with an exclusive capture set can be widened to a reference with a read-only set. For instance, the following is OK:
+```scala
+val a: Ref^ = Ref()
+val b1: Ref^{a.rd} = a
+val b2: Ref^{cap.rd} = a
+```
+
+## Read-Only Capsets
+
+If we consider subtyping and subcapturing, we observe what looks like a contradiction: `x.rd` is seen as a restricted capability, so `{x.rd}` should subcapture `{x}`. Yet, we have seen in the example above that sometimes it goes the other way: `a`'s capture set is either `{a}` or `{cap}`, yet `a` can be used to define `b1` and `b2`, with capture sets `{a.rd}` and `{cap.rd}`, respectively.
+
+The contradiction can be explained by noting that we use a capture set in two different roles.
+
+First, and as always, a capture set defines _retained capabilities_ that may or may be not used by a value. More capabilities give larger types, and the empty capture set is the smallest set according to that ordering. That makes sense: If a higher-order function like `map` is willing to accept a function `A => B` that can have arbitrary effects it's certainly OK to pass a pure function of type `A -> B` to it.
+
+But for mutations, we use a capture set in a second role, in which it defines a set of _access permissions_. If we have a `Ref^`, we can access all its methods, but if we have a `Ref^{cap.rd}`, we can access only regular methods, not update methods. From that viewpoint a mutable type with exclusive capabilities lets you do more than a mutable type with just read-only capabilities. So by the Liskov substitution principle, sets with exclusive capabilities subcapture sets with only read-only capabilities.
+
+The contradiction can be solved by distinguishing these two roles. For access permissions, we express read-only sets with an additional _qualifier_ `RD`. That qualifier is used only in the formal theory and the implementation, it currently cannot be expressed in source.
+We add an implicit read-only qualifier `RD` to all capture sets on mutable types that consist only of shared or read-only capabilities.
+So when we write
+```scala
+val b1: Ref^{a.rd} = a
+```
+we really mean
+```scala
+val b1: Ref^{a.rd}.RD = a
+```
+
+The subcapturing theory for sets is then as before, with the following additional rules:
+
+ - `C <: C.RD`
+ - `C₁.RD <: C₂.RD` if `C₍ <: C₂`
+ - `{x, ...}.RD = {x.rd, ...}.RD`
+ - `{x.rd, ...} <: {x, ...}`
+
+
+
+
