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