Update scoped-caps.md

Author: bracevac

docs/_docs/reference/experimental/capture-checking/scoped-caps.md

@@ -14,18 +14,18 @@ We will discuss three distinct kinds of `cap` in this chapter:
 
 **Local caps**: Every class, method body, and block has its own local `cap`. It abstracts over the capabilities used inside that scope, representing them by a single name to the outside world. Local caps form a subcapturing hierarchy based on lexical nesting.
 
-**Parameter caps**: When `cap` appears in a function parameter type (e.g., `def foo(x: T^)`), it gets its own cap scoped to that parameter. At call sites, parameter caps are instantiated to the actual capabilities passed in.
+**Parameter caps**: When `cap` appears in a function parameter type (e.g., `def foo(x: T^)`), it gets its own `cap` scoped to that parameter. At call sites, parameter caps are instantiated to the actual capabilities passed in.
 
-**Result caps**: When `cap` appears in a function result type (e.g., `def foo(x: T): U^`), it becomes an existentially-bound cap that describes what the caller receives. Unlike local caps, result caps do _not_ subsume the enclosing scope's `cap`.
+**Result caps**: When `cap` appears in a function result type (e.g., `def foo(x: T): U^`), it becomes an existentially-bound `cap` that describes what the caller receives.
 
 So, when writing `T^` (shorthand for `T^{cap}`), `cap` is a way of saying "captures something" without
 naming what it is precisely, and depending of the context occurrence of such `cap`s, the capture checker imposes
-restrictions on which capabilities are allowed to flow into them. We will further expand on this idea
+restrictions on which capabilities are allowed to flow into them by means of subcapturing. We will further expand on this idea
 (and other kinds of `cap`) later when discussing [separation checking](separation-checking.md).
 
 Another analogy for the different `cap`s is that they are some form of implicitly named existential or abstract self-capture set attached to elements of the program structure, e.g., scopes, parameters, or return values.
 
-## Subcapturing and Levels
+## Local Caps
 
 Local `cap`s form a subcapturing hierarchy based on lexical nesting: a nested scope's local `cap` subsumes its enclosing scope's local `cap`. This makes sense because the inner scope can use any capability available in the outer scope
 as well as locally defined ones. At the top level, there is a true universal `cap` — the local `cap` of the global scope — which all other local `cap`s ultimately subsume:
@@ -78,7 +78,7 @@ def process(fs: FileSystem^): Unit =
   val f: () -> Unit = () => fs.read()  // Error: fs cannot flow into {}
 ```
 
-The closure is declared pure (`() -> Unit`), meaning its local cap is the empty set. The capability `fs` cannot flow into an empty set, so the checker rejects this.
+The closure is declared pure (`() -> Unit`), meaning its local `cap` is the empty set. The capability `fs` cannot flow into an empty set, so the checker rejects this.
 
 ### Visibility and Widening
 
@@ -90,55 +90,85 @@ def test(fs: FileSystem^): Logger^ =
   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`.
+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`.
 
-## Existential Binding in Function Types
+### Local Caps of Classes
 
-So far we've discussed local `cap`s that follow the lexical nesting hierarchy. But `cap` can also appear in function parameter and result types, where special binding rules apply.
+A class receives its own local `cap` for the scope of its body. This `cap` serves as a template for
+a fresh `cap` that will be attached to each instance of the class. Inside the class body, references
+to the class's `cap` are implicitly prefixed by the path `this`:
 
-### Result Caps
+```scala
+class Logger(fs: FileSystem^): // local cap₁
+  // Logger has its own local cap₁, accessed as this.cap₁
+  val file: File^ = fs.open("log.txt")  // File^{this.cap₁}
+  def log(msg: String): Unit = file.write(msg)
+```
 
-Consider this method:
+When a class inherits from other classes or traits, the `cap`s of all supertypes in the `extends`
+clause are essentially unified with the `cap` of the current class. This unification happens because
+all inherited members are accessed through `this`, and hence the local `cap`s will conform through
+subtyping with each other:
 
 ```scala
-def makeLogger(fs: FileSystem^): Logger^ = new Logger(fs)
+trait Super: // local cap₁
+  val doSomething: () => Unit // () ->{cap₁} Unit
+
+class Logger(fs: FileSystem^) extends Supper: // local cap₂
+  val file: File^ = fs.open("log.txt") // File^{cap₂}
+  def log(msg: String): Unit = file.write(msg)
+  val doSomething = () => log("hello") // ok, since {file} <: {this.cap₂} =:= {this.cap₁}
 ```
 
-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.
+As explained in [Capture Checking of Classes](classes.md), the capture checker infers and verifies
+constraints on the contents of a class's `cap` through its self-type, reporting any inconsistencies.
+
+When creating an instance, the class's template `cap` is substituted with a fresh `cap` specific to
+the new object:
 
-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₂}
+def test(fs: FileSystem^) =
+  val logger = Logger(fs)  // Fresh logger.cap for this instance, capturing fs
+  logger
 ```
-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₂`.
+Note that the `cap` of attached to `logger` subcaptures the local `cap` of method `test` in accordance
+to the rules outlined earlier.
+
+Conceptually, a class' local `cap` behaves like an implicit [capture-set member](polymorphism.md#capability-members)
+present in the class and all its supertypes:
 
-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₂}
+class Logger(fs: FileSystem^):
+  type Cap^
+  val file: File^{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.
 
-### Why Result Caps Don't Subcapture Local Caps
+## Parameter and Result Caps in Function Types
 
-Result `cap`s do _not_ subsume the enclosing scope's local `cap`. Result `cap`s are bound at the function boundary, not within the function body:
+So far we've discussed local `cap`s that follow the lexical nesting hierarchy. But `cap` can also appear in function parameter and result types, where special binding rules apply.
+
+### Existential Binding
+
+Consider this method:
 
 ```scala
-def outer(): () -> File^ =
-  val localFile: File^ = openFile()
-  () => localFile  // Error!
+def makeLogger(fs: FileSystem^): Logger^ = new Logger(fs)
 ```
 
-The return type `() -> File^` contains an existentially-bound result cap. If this result cap subcaptured `outer`'s local cap, then `localFile` could flow into it, and the local file would escape. The whole point of the existential is to describe what the _caller_ receives — it must not allow capabilities from the callee's scope to leak out.
-
-In contrast, a local cap inside a function body _does_ subcapture the enclosing local cap:
+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
-def outer(): Unit =
-  val f: File^ = openFile()  // This ^ is outer's local cap
-  val g: () => Unit = () => f.read()  // OK: closure's local cap subcaptures outer's local cap
+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₂`.
 
-Here the closure's local cap can absorb `f` because both are nested within `outer`.
+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.
 
 ### Expansion Rules for Function Types
 
@@ -182,6 +212,40 @@ To summarize:
 
 Later sections on [capability classifiers](classifiers.md) will add a controlled mechanism that permits capabilities to escape their level for situations where this would be desirable.
 
+### Parameter Caps and Local Caps
+
+Inside the function body, parameter caps are at the **same level** as the function's local `cap`. This means the function's local `cap` can subsume capabilities from parameters:
+
+```scala
+def process(x: File^/* parameter {cap₁} */): Unit = /* local cap₂ */
+  val y: File^/*{cap₂}*/ = x  // OK: x's cap is at process's level, same as process's local cap
+  val f: () =>/*{cap₂}*/ Unit = () => x.read()  // OK: closure's local cap subsumes x
+```
+
+The parameter `x` has a capability at `process`'s level. The local `cap` of `process` (and any nested closures) can subsume it because they're at the same level or more deeply nested.
+
+### Result Caps Don't Subsume Local Caps
+
+Result `cap`s do _not_ subsume the enclosing scope's local `cap`. Result `cap`s are bound at the function boundary, not within the function body:
+
+```scala
+def outer(): () -> File^ =
+  val localFile: File^ = openFile()
+  () => localFile  // Error!
+```
+
+The return type `() -> File^` contains an existentially-bound result `cap`. If this result `cap` subsumed `outer`'s local `cap`, then `localFile` could flow into it, and the local file would escape. The whole point of the existential is to describe what the _caller_ receives — it must not allow capabilities from the callee's scope to leak out.
+
+In contrast, a local `cap` inside a function body _does_ subsume the enclosing local `cap`:
+
+```scala
+def outer(): Unit =
+  val f: File^ = openFile()  // This ^ is outer's local cap
+  val g: () => Unit = () => f.read()  // OK: closure's local cap subsumes outer's local cap
+```
+
+Here the closure's local `cap` can absorb `f` because both are nested within `outer`.
+
 ## Comparison with Rust Lifetimes
 
 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.