Skip to content

Commit 169dd69

Browse files
bracevacbracevac
committed
Update CC language reference
1 parent 67708cb commit 169dd69

File tree

1 file changed

+129
-17
lines changed
  • docs/_docs/reference/experimental

1 file changed

+129
-17
lines changed

‎docs/_docs/reference/experimental/cc.md

+129-17
Original file line numberDiff line numberDiff line change
@@ -726,41 +726,153 @@ Reach capabilities take the form `x*` where `x` is syntactically a regular capab
726726
It is sometimes convenient to write operations that are parameterized with a capture set of capabilities. For instance consider a type of event sources
727727
`Source` on which `Listener`s can be registered. Listeners can hold certain capabilities, which show up as a parameter to `Source`:
728728
```scala
729-
class Source[X^]:
730-
private var listeners: Set[Listener^{X^}] = Set.empty
731-
def register(x: Listener^{X^}): Unit =
732-
listeners += x
729+
class Source[X^]:
730+
private var listeners: Set[Listener^{X}] = Set.empty
731+
def register(x: Listener^{X}): Unit =
732+
listeners += x
733733

734-
def allListeners: Set[Listener^{X^}] = listeners
734+
def allListeners: Set[Listener^{X}] = listeners
735735
```
736736
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
737-
we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X^`. The `register` method takes a listener of this type
737+
we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X`. The `register` method takes a listener of this type
738738
and assigns it to the variable.
739739

740-
Capture set variables `X^` are represented as regular type variables with a
741-
special upper bound `CapSet`. For instance, `Source` could be equivalently
740+
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.
741+
742+
Under the hood, such capture-set variables are represented as regular type variables within the special interval
743+
`>: CapSet <: CapSet^`.
744+
For instance, `Source` from above could be equivalently
742745
defined as follows:
743746
```scala
744-
class Source[X <: CapSet^]:
745-
...
747+
class Source[X >: CapSet <: CapSet^]:
748+
...
746749
```
747-
`CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only purpose is to identify capture set type variables and types. Capture set variables can be inferred like regular type variables. When they should be instantiated explicitly one uses a capturing
748-
type `CapSet`. For instance:
750+
`CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only
751+
purpose is to identify type variables which are capture sets. In non-capture-checked
752+
usage contexts, the type system will treat `CapSet^{a}` and `CapSet^{a,b}` as the type `CapSet`, whereas
753+
with capture checking enabled, it will take the annotated capture sets into account,
754+
so that `CapSet^{a}` and `CapSet^{a,b}` are distinct.
755+
This representation based on `CapSet` is subject to change and
756+
its direct use is discouraged.
757+
758+
Capture-set variables can be inferred like regular type variables. When they should be instantiated
759+
explicitly one supplies a concrete capture set. For instance:
749760
```scala
750-
class Async extends caps.Capability
761+
class Async extends caps.Capability
751762

752-
def listener(async: Async): Listener^{async} = ???
763+
def listener(async: Async): Listener^{async} = ???
753764

754-
def test1(async1: Async, others: List[Async]) =
755-
val src = Source[CapSet^{async1, others*}]
756-
...
765+
def test1(async1: Async, others: List[Async]) =
766+
val src = Source[{async1, others*}]
767+
...
757768
```
758769
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:
759770
```scala
760771
src.register(listener(async1))
761772
others.map(listener).foreach(src.register)
762773
val ls: Set[Listener^{async, others*}] = src.allListeners
763774
```
775+
A common use-case for explicit capture parameters is describing changes to the captures of mutable fields, such as concatenating
776+
effectful iterators:
777+
```scala
778+
class ConcatIterator[A, C^](var iterators: mutable.List[IterableOnce[A]^{C}]):
779+
def concat(it: IterableOnce[A]^): ConcatIterator[A, {this.C, it}]^{this, it} =
780+
iterators ++= it // ^
781+
this // track contents of `it` in the result
782+
```
783+
In such a scenario, we also should ensure that any pre-existing alias of a `ConcatIterator` object should become
784+
inaccessible after invoking its `concat` method. This is achieved with mutation and separation tracking which are
785+
currently in development.
786+
787+
Finally, analogously to type parameters, we can lower- and upper-bound capability parameters where the bounds consist of concrete capture sets:
788+
```scala
789+
def main() =
790+
// We can close over anything branded by the 'trusted' capability, but nothing else
791+
def runSecure[C^ >: {trusted} <: {trusted}](block: () ->{C} Unit): Unit = ...
792+
793+
// This is a 'brand" capability to mark what can be mentioned in trusted code
794+
object trusted extends caps.Capability
795+
796+
// These capabilities are trusted:
797+
val trustedLogger: Logger^{trusted}
798+
val trustedChannel: Channel[String]^{trusted}
799+
// These aren't:
800+
val untrustedLogger: Logger^
801+
val untrustedChannel: Channel[String]^
802+
803+
runSecure: () =>
804+
trustedLogger.log("Hello from trusted code") // ok
805+
806+
runSecure: () =>
807+
trustedChannel.send("I can send") // ok
808+
trustedLogger.log(trustedChannel.recv()) // ok
809+
810+
runSecure: () => "I am pure and that's ok" // ok
811+
812+
runSecure: () =>
813+
untrustedLogger.log("I can't be used") // error
814+
untrustedChannel.send("I can't be used") // error
815+
```
816+
The idea is that every capability derived from the marker capability `trusted` (and only those) are eligible to be used in the `block` closure
817+
passed to `runSecure`. We can enforce this by an explicit capability parameter `C` constraining the possible captures of `block` to the interval `>: {trusted} <: {trusted}`.
818+
819+
Note that since capabilities of function types are covariant, we could have equivalently specified `runSecure`'s signature using implicit capture polymorphism to achieve the same behavior:
820+
```scala
821+
def runSecure(block: () ->{trusted} Unit): Unit
822+
```
823+
824+
## Capability Members
825+
826+
Just as parametrization by types can be equally expressed with type members, we could
827+
also define the `Source[X^]` class above could using a _capability member_:
828+
```scala
829+
class Source:
830+
type X^
831+
private var listeners: Set[Listener^{this.X}] = Set.empty
832+
... // as before
833+
```
834+
Here, we can refer to capability members using paths in capture sets (such as `{this.X}`). Similarly to type members,
835+
capability members can be upper- and lower-bounded with capture sets:
836+
```scala
837+
trait Thread:
838+
type Cap^
839+
def run(block: () ->{this.Cap} -> Unit): Unit
840+
841+
trait GPUThread extends Thread:
842+
type Cap^ >: {cudaMalloc, cudaFree} <: {caps.cap}
843+
```
844+
Since `caps.cap` is the top element for subcapturing, we could have also left out the
845+
upper bound: `type Cap^ >: {cudaMalloc, cudaFree}`.
846+
847+
We conclude with a more advanced example, showing how capability members and paths to these members can prevent leakage
848+
of labels for lexically-delimited control operators:
849+
```scala
850+
trait Label extends Capability:
851+
type Fv^ // the capability set occurring freely in the `block` passed to `boundary` below.
852+
853+
def boundary[T, C^](block: Label{type Fv = {C} } ->{C} T): T = ??? // ensure free caps of label and block match
854+
def suspend[U](label: Label)[D^ <: {label.Fv}](handler: () ->{D} U): U = ??? // may only capture the free capabilities of label
855+
856+
def test =
857+
val x = 1
858+
boundary: outer =>
859+
val y = 2
860+
boundary: inner =>
861+
val z = 3
862+
val w = suspend(outer) {() => z} // ok
863+
val v = suspend(inner) {() => y} // ok
864+
val u = suspend(inner): () =>
865+
suspend(outer) {() => w + v} // ok
866+
y
867+
suspend(outer): () =>
868+
println(inner) // error (would leak the inner label)
869+
x + y + z
870+
```
871+
A key property is that `suspend` (think `shift` from delimited continuations) targeting a specific label (such as `outer`) should not accidentally close over labels from a nested `boundary` (such as `inner`), because they would escape their defining scope this way.
872+
By leveraging capability polymorphism, capability members, and path-dependent capabilities, we can prevent such leaks from occurring at compile time:
873+
874+
* `Label`s store the free capabilities `C` of the `block` passed to `boundary` in their capability member `Fv`.
875+
* When suspending on a given label, the suspension handler can capture at most the capabilities that occur freely at the `boundary` that introduced the label. That prevents mentioning nested bound labels.
764876

765877
## Compilation Options
766878

0 commit comments

Comments
 (0)