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.

classIteratorList(privatevariterators: mutable.List[Iterator[A]^])://                                            ^ this cap will be instantiated with whatever is in the initial list// ...def+=(it:Iterator[A]^)= iterators+= itvalxs=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.

classIteratorList[C^](privatevariterators: mutable.List[Iterator[A]^{C}]):// ...def+=(it:Iterator[A]^{C})= iterators+= itvalxs=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.

Nit: I thinkflow is a vague word. Maybe "The level determines where a capability can be part of: it can be a part ofcaps 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?

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

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