CC Language Reference Improvements v2 (#23818)

Author: odersky

docs/_docs/reference/experimental/capture-checking/how-to-use.md

@@ -6,7 +6,48 @@ nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-che
 
 ## Enabling Capture Checking
 
-TODO
+Use Scala 3 nightly for the latest features and fixes.
+
+Add this import in any file that uses capture checking:
+```scala
+import language.experimental.captureChecking
+```
+
+### Separation Checking
+
+Requires the import above:
+```scala
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+```
+
+### SBT Project Template
+
+Alternatively, you can clone a pre-defined SBT project to get
+started: https://github.com/lampepfl/scala3-cc-template
+
+### The REPL/Scala-CLI
+
+Using the command line through explicit parameters:
+```bash
+scala -S 3.nightly -language:experimental.captureChecking
+```
+or when reading from a file:
+```scala
+// foo.scala:
+//> using scala 3.nightly
+import language.experimental.captureChecking
+...
+```
+Then, it suffices to run
+```bash
+scala foo.scala
+```
+
+## API Documentation
+
+Scaladoc supports capture checking. The nightly standard library API docs have it enabled by default:
+https://nightly.scala-lang.org/api/
 
 ## Compilation Options
 

tests/neg-custom-args/captures/classifiers-secondclass.check

@@ -0,0 +1,39 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/classifiers-secondclass.scala:41:28 ----------------------
+41 | parReduce(1 to 1000): (a, b) => // error
+ | ^
+ |Found: (a: Int, b: Int) ->{f.write, f.read} Int
+ |Required: (Int, Int) ->{cap.only[Read]} Int
+ |
+ |Note that capability f.write is not included in capture set {cap.only[Read]}.
+ |
+ |where: cap is a fresh root capability created in anonymous function of type (f²: Levels.File^): Unit when checking argument to parameter op of method parReduce
+42 | f.write(42) // the error stems from here
+43 | a + b + f.read() // ok
+ |
+ | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/classifiers-secondclass.scala:53:30 ----------------------
+53 | parReduce(1 to 1000): (a, b) => // error
+ | ^
+ |Found: (a: Int, b: Int) ->{f.write, f.read, g.read} Int
+ |Required: (Int, Int) ->{cap.only[Read]} Int
+ |
+ |Note that capability f.write is not included in capture set {cap.only[Read]}.
+ |
+ |where: cap is a fresh root capability created in anonymous function of type (g²: Levels.File^): Unit when checking argument to parameter op of method parReduce
+54 | f.write(42) // the error stems from here
+55 | a + b + f.read() + g.read() // ok
+ |
+ | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/classifiers-secondclass.scala:56:30 ----------------------
+56 | parReduce(1 to 1000): (a, b) => // error
+ | ^
+ |Found: (a: Int, b: Int) ->{g.write} Int
+ |Required: (Int, Int) ->{cap.only[Read]} Int
+ |
+ |Note that capability g.write is not included in capture set {cap.only[Read]}.
+ |
+ |where: cap is a fresh root capability created in anonymous function of type (g²: Levels.File^): Unit when checking argument to parameter op of method parReduce
+57 | g.write(42) // the error stems from here
+58 | 0
+ |
+ | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/classifiers-secondclass.scala

@@ -1,67 +1,61 @@
 import language.experimental.captureChecking
 import language.experimental.separationChecking
+import language.experimental.erasedDefinitions
+
 import caps.*
 
 // Test inspired by the "Gentrification Gone too Far?" paper
 object Levels:
 
+ /* User-defined capability classifiers */
  trait Read extends Classifier, SharedCapability
  trait ReadWrite extends Classifier, SharedCapability
 
  trait File(val name: String):
- val r: Read^
- val rw: ReadWrite^
- // operations guarded by boxed capability members
+ // file-specific capability members, these are ensured to be erased
+ erased val r: Read^
+ erased val rw: ReadWrite^
+ // operations guarded by capability members
  val read: () ->{r} Int
  val write: Int ->{rw} Unit
 
  object File:
  def apply(s: String): File^ = new File(s) {
- val r = new Read {}
- val rw = new ReadWrite {}
+ erased val r = new Read {}
+ erased val rw = new ReadWrite {}
  val read = () =>
  println(s"Reading from $name with capability $r")
  42
  val write = (i: Int) =>
  println(s"Writing $i to $name with capability $rw")
  }
 
- // Unfortunately, we do not have @use lambdas yet
- trait UseFunction[U]:
- def apply[C^](f: File^{C}): U
-
- def withFile[U](name: String)(block: UseFunction[U]): U = block(File(name)) // unrestricted use of files & other capabilities
+ def withFile[U](name: String)(block: File^ => U): U = block(File(name)) // unrestricted use of files & other capabilities
  def parReduce[U](xs: Seq[U])(op: (U, U) ->{cap.only[Read]} U): U = xs.reduce(op) // only Read-classified allowed
 
  @main def test =
- withFile("foo.txt"):
- new UseFunction[Unit]:
- def apply[C^](f: File^{C}): Unit =
- f.read() // ok
- parReduce(1 to 1000): (a, b) =>
- a * b * f.read() // ok
- parReduce(1 to 1000): (a, b) => // error
- f.write(42) // the error stems from here
- a + b + f.read() // ok
- f.write(42) // ok, unrestricted access to file
+ withFile("foo.txt"): f =>
+ f.read() // ok
+ parReduce(1 to 1000): (a, b) =>
+ a * b * f.read() // ok
+ parReduce(1 to 1000): (a, b) => // error
+ f.write(42) // the error stems from here
+ a + b + f.read() // ok
+ f.write(42) // ok, unrestricted access to file
 
  def testMulti =
- withFile("foo.txt"):
- new UseFunction[Unit]:
- def apply[C^](f: File^{C}): Unit =
- withFile("bar.txt"):
- new UseFunction[Unit]:
- def apply[C^](g: File^{C}): Unit =
- f.read() // ok
- g.read() // ok
- parReduce(1 to 1000): (a, b) =>
- a * b * f.read() + g.read() // ok
- parReduce(1 to 1000): (a, b) => // error
- f.write(42) // the error stems from here
- a + b + f.read() + g.read() // ok
- parReduce(1 to 1000): (a, b) => // error
- g.write(42) // the error stems from here
- 0
- f.write(42) // ok, unrestricted access to file
- g.write(42) // ok, unrestricted access to file
+ withFile("foo.txt"): f =>
+ withFile("bar.txt"): g =>
+ f.read() // ok
+ g.read() // ok
+ parReduce(1 to 1000): (a, b) =>
+ a * b * f.read() + g.read() // ok
+ parReduce(1 to 1000): (a, b) => // error
+ f.write(42) // the error stems from here
+ a + b + f.read() + g.read() // ok
+ parReduce(1 to 1000): (a, b) => // error
+ g.write(42) // the error stems from here
+ 0
+ f.write(42) // ok, unrestricted access to file
+ g.write(42) // ok, unrestricted access to file