Add caps.immutable wrapper

Author: odersky

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -790,22 +790,44 @@ class CheckCaptures extends Recheck, SymTransformer:
           selType
     }//.showing(i"recheck sel $tree, $qualType = $result")
 
-    /** Recheck applications, with special handling of unsafeAssumePure.
+    /** Recheck `caps.unsafe.unsafeAssumePure(...)` */
+    def applyAssumePure(tree: Apply, pt: Type)(using Context): Type =
+      val arg :: Nil = tree.args: @unchecked
+      val argType0 = recheck(arg, pt.stripCapturing.capturing(FreshCap(Origin.UnsafeAssumePure)))
+      val argType =
+        if argType0.captureSet.isAlwaysEmpty then argType0
+        else argType0.widen.stripCapturing
+      capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType")
+      super.recheckFinish(argType, tree, pt)
+
+    /** Recheck `caps.immutable(...)` */
+    def applyImmutable(tree: Apply)(using Context): Type =
+      val arg :: Nil = tree.args: @unchecked
+      def imm = new TypeMap:
+        def apply(t: Type) = t match
+          case t @ CapturingType(parent, _)
+          if parent.derivesFromMutable && variance > 0 =>
+            t.derivedCapturingType(apply(parent), CaptureSet.emptyOfMutable)
+          case _ =>
+            mapOver(t)
+      val opProto = // () ?-> <?>
+        defn.FunctionType(0, isContextual = true).appliedTo(WildcardType)
+      recheck(arg, opProto).stripCapturing match
+        case defn.ContextFunctionType(Nil, resType) => imm(resType)
+
+    /** Recheck applications, with special handling of unsafeAssumePure,
+     *  unsafeDiscardUses, and immutable.
      *  More work is done in `recheckApplication`, `recheckArg` and `instantiate` below.
      */
     override def recheckApply(tree: Apply, pt: Type)(using Context): Type =
       val meth = tree.fun.symbol
       if meth == defn.Caps_unsafeAssumePure then
-        val arg :: Nil = tree.args: @unchecked
-        val argType0 = recheck(arg, pt.stripCapturing.capturing(FreshCap(Origin.UnsafeAssumePure)))
-        val argType =
-          if argType0.captureSet.isAlwaysEmpty then argType0
-          else argType0.widen.stripCapturing
-        capt.println(i"rechecking unsafeAssumePure of $arg with $pt: $argType")
-        super.recheckFinish(argType, tree, pt)
+        applyAssumePure(tree, pt)
       else if meth == defn.Caps_unsafeDiscardUses then
         val arg :: Nil = tree.args: @unchecked
         withDiscardedUses(recheck(arg, pt))
+      else if meth == defn.Caps_immutable then
+        applyImmutable(tree)
       else
         val res = super.recheckApply(tree, pt)
         includeCallCaptures(meth, res, tree)

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -1031,6 +1031,7 @@ class Definitions {
     @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains")
     @tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains")
     @tu lazy val Caps_containsImpl: TermSymbol = Caps_ContainsModule.requiredMethod("containsImpl")
+    @tu lazy val Caps_immutable: TermSymbol = CapsModule.requiredMethod("immutable")
 
   @tu lazy val PureClass: ClassSymbol = requiredClass("scala.caps.Pure")
 
@@ -2098,7 +2099,7 @@ class Definitions {
     RequiresCapabilityAnnot,
     captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass,
     ConsumeAnnot, UseAnnot, ReserveAnnot,
-    CapsUnsafeModule, CapsUnsafeModule.moduleClass,
+    CapsUnsafeModule, CapsUnsafeModule.moduleClass, Caps_immutable,
     CapsInternalModule, CapsInternalModule.moduleClass,
     RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot)
 

docs/_docs/reference/experimental/capture-checking/mutability.md

@@ -339,3 +339,34 @@ The subcapturing theory for sets is then as before, with the following additiona
  - `{x, ...}.RD = {x.rd, ...}.RD`
  - `{x.rd, ...} <: {x, ...}`
 
+## The `immutable` Wrapper
+
+We often want to create a mutable data structure like an array, initialize by assigning to its elements and then return the array as an immutable type that does not
+capture any capabilities. This can be achieved using the `immutable` wrapper.
+
+As an example, consider a class `Arr` which is modelled after `Array` and its immutable counterpart `IArr`:
+
+```scala
+class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
+  private val arr: Array[T] = new Array[T](len)
+  def get(i: Int): T = arr(i)
+  update def update(i: Int, x: T): Unit = arr(i) = x
+type IArr[T] = Arr[T]^{}
+```
+
+The `immutable` wrapper allows us to go from an `Arr` to an `IArr`, safely:
+```scala
+import caps.immutable
+
+val f: IArr[String] = immutable:
+  val a = Arr[String](2)
+  a(0) = "hello"
+  a(1) = "world"
+  a
+```
+The `immutable` method is defined in `caps` like this:
+```scala
+def immutable[T](op: -> T): T = op
+```
+It takes a pure by-name parameter and returns its result. But the actual return type after capture checking is special. Instead of just `T` as in the declaration above suggests, it's `T` where every covariant occurrence of a `Mutable` type gets its capture set mapped to `{}`.
+

library/src/scala/caps/package.scala

@@ -123,6 +123,7 @@ final class reserve extends annotation.StaticAnnotation
  *  environment.
  */
 @experimental
+@deprecated(since = "3.8.0")
 final class use extends annotation.StaticAnnotation
 
 /** A trait that used to allow expressing existential types. Replaced by
@@ -132,6 +133,12 @@ final class use extends annotation.StaticAnnotation
 @deprecated
 sealed trait Exists extends Capability
 
+/** A wrapper that strips all covariant capture sets from Mutable types in the
+ *  result of pure operation `op`, turning them into immutable types.
+ */
+@experimental
+def immutable[T](op: -> T): T = op
+
 @experimental
 object internal:
 

tests/neg-custom-args/captures/immutable.check

@@ -0,0 +1,22 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/immutable.scala:13:20 ------------------------------------
+13 |  val b = immutable(a) // error
+   |                    ^
+   |                    Found:    () ?->{a} Arr[String]^{a}
+   |                    Required: () ?-> <?>
+   |
+   |                    Note that capability a is not included in capture set {}.
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/immutable.scala:22:4 -------------------------------------
+21 |  immutable:
+22 |    mkExclusive() // error
+   |  ^
+   |  Capability cap outlives its scope: it leaks into outer capture set 's1 of method test3.
+   |  The leakage occurred when trying to match the following types:
+   |
+   |  Found:    EX^{cap}
+   |  Required: EX^'s1
+   |
+   |  where:    cap is a root capability associated with the result type of (): EX^
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/immutable.scala

@@ -0,0 +1,23 @@
+import caps.*
+
+class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
+  private val arr: Array[T] = new Array[T](len)
+  def get(i: Int): T = arr(i)
+  update def update(i: Int, x: T): Unit = arr(i) = x
+
+
+def test2 =
+  val a = Arr[String](2)
+  a(0) = "1"
+  a(1) = "2"
+  val b = immutable(a) // error
+  b
+
+class EX
+
+def mkExclusive(): EX^ = ???
+
+def test3 =
+  immutable:
+    mkExclusive() // error
+

tests/pending/pos-custom-args/captures/immutable-cycle.scala

@@ -0,0 +1,15 @@
+import caps.*
+
+class Node(val payload: Int) extends Mutable:
+  var next: Node = ???
+
+
+type INode = Node^{}
+
+def cycle(x: Int, y: Int): (INode, INode) =
+  immutable:
+    val a = Node(x)
+    val b = Node(y)
+    a.next = b
+    b.next = a
+    (a, b)

tests/pos-custom-args/captures/immutable.scala

@@ -0,0 +1,26 @@
+import language.experimental.captureChecking
+import caps.*
+
+class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
+  private val arr: Array[T] = new Array[T](len)
+  def get(i: Int): T = arr(i)
+  update def update(i: Int, x: T): Unit = arr(i) = x
+
+
+def test2 =
+  val a = immutable:
+    val a = Arr[String](2)
+    a(0) = "1"
+    a(1) = "2"
+    a
+  val _: Arr[String]^{} = a
+
+  val a2 = immutable:
+    val a = Arr[String](2)
+    val b = Arr[String](2)
+    a(0) = "1"
+    a(1) = "2"
+    b(0) = "1"
+    b(1) = "2"
+    (a, b)
+  val _: (Arr[String]^{}, Arr[String]^{}) = a2