Update CC Docs Until scoped-caps.md

[bracevac]

Continuation of #24626

[skip ci]

[natsukagami]

Suggested change

	def collect[T, C^](fs: Set[Future[T]]^{C})(using Async^): Stream[Future[T]^{C}] =
	def collect[T, C^](fs: Set[Future[T]^{C}])(using Async^): Stream[Future[T]^{C}] =

[natsukagami]

I think this is a poor example, as it instantly leads the reader into writing this (very buggy, doesn't guarantee anything until separation checking) code.

The problem with mutable collections with non-type-parameter element types is that you cannot use implicit capture polymorphism: they get instantiated with the elements at the construction of the collection.

class IteratorList(private var iterators: mutable.List[Iterator[A]^]):
  //                                            ^ this cap will be instantiated with whatever is in the initial list
  // ...
  def +=(it: Iterator[A]^) = iterators += it
  
val xs = IteratorList(mutable.List.empty) // forcefully instantiated to {}

(also we don't have a name to refer to the capture set of the elements, when we write the += method)

Therefore, we need a capture set variable, to allow the user/inference to specify a capture set suitable for the whole usage of the collection.

class IteratorList[C^](private var iterators: mutable.List[Iterator[A]^{C}]):
  // ...
  def +=(it: Iterator[A]^{C}) = iterators += it
  
val xs = IteratorList(mutable.List.empty)
xs += Iterator(async)
xs += Iterator(io)
// inference will (probably) find out that xs: IteratorList[{async, io}] 

Note that this capture set will not change, it's part of the type: it means you have to be able to name all the captures of all the elements at the point of creating the collection. If you want a growing capture set, it's not sound until separation checking.

[natsukagami]

Suggested change

	- `f1` is at `Outer`'s level, i.e., `f` subcaptures local `cap₁`.
	- `f1` is at `Outer`'s level, i.e., `f1` subcaptures local `cap₁`.

[natsukagami]

Nit: I think flow is a vague word. Maybe "The level determines where a capability can be part of: it can be a part of caps at the same level or more deeply nested..." or something like "assigned to"?

Update: I think we used in a lot of places, so maybe it's fine?

[natsukagami]

Suggested change

	- By lexical lifetime, `{cap₂} <: {cap₃}` holds, but it does **not** hold that `{cap₃} <: {cap₂}`. Hence,
	- By lexical nesting, `{cap₂} <: {cap₃}` holds, but it does **not** hold that `{cap₃} <: {cap₂}`. Hence,

Lifetimes? Are we Rust? 🦀

[natsukagami]

Perhaps we should say something about the withFile[T] pattern here?

[natsukagami]

What should A => B => C be extended to? I think it's quite unclear here

[natsukagami]

Suggested change

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.

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 of a reference then acts as an upper bound of the reference itself: it only lives as long as all the capabilities it contains are visible.