Drop @capability annotations #20396

odersky · 2024-05-13T14:34:38Z

Replace with references that inherit trait Capability.

Also: Handle tracked vals in classes.

As a next step, addCaptureRefinements should use the tracked logic for all capturing parameters. Right now, we create a fresh capture set variable instead, but that is too loose.

propensive · 2024-05-13T22:13:29Z

library/src/scala/annotation/capability.scala

@@ -11,4 +11,6 @@ import annotation.experimental
 *  THere, the capture set of any instance of `CanThrow` is assumed to be
 *  `{*}`.
 */
-@experimental final class capability extends StaticAnnotation
+@experimental
+@deprecated("To make a class a capability, let it derive from the `Capability` trait instead")


Why not phrase this as, ...let it extend the...? derives has an established meaning which isn't what's intended here.

odersky · 2024-05-19T11:50:31Z

Summary of changes:

Drop @capability
Instead allow a class to extend a new trait caps.Capablity. So instead of @capability class IO it would be class IO extends caps.Capability.
The treatment of the two is different, though. @capability added ^ to references during setup. The new capability classes are instead treated as primitive maximal capabilities without having cap in their capture set.
We also retract the convention that capture sets in the parents of a class are somehow inherited by references to those classes.
We also refine box adaptation not to create spurious captureset variables in function types, which leads to more references with function typed being kept as singletons instead of being widened.
Finally, we refine the scheme that adds parameter refinements to class types. We now refine only if the parameter has a capture set (for the others it does not matter) and is not tracked (since tracked parameter dependencies are already handled anyway)

noti0na1

There are still some import of annotation.capability can be deleted; the document should be updated as well.

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

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

noti0na1 · 2024-05-22T13:28:12Z

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

@@ -2273,6 +2273,9 @@ object Types extends TypeUtils {
    /** Is this reference the generic root capability `cap` ? */
    def isRootCapability(using Context): Boolean = false

+    /** Is this reference capability that does not derive from another capability ? */


I am a little confused when we should use isMaxCapability or isRootCapability? since "max capability" should cover the cases of "root capability". For example, inside subsumes, I feel isMaxCapability is a better choice.

noti0na1 · 2024-05-22T13:32:43Z

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

   |    of an enclosing function literal with expected type () ?->{cap1} I
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/byname.scala:4:2 -----------------------------------------
 4 |  def f() = if cap1 == cap1 then g else g // error
   |  ^
-   |  Found:    (x$0: Int) ->{cap2} Int
-   |  Required: (x$0: Int) -> Int
+   |  Found:    ((x$0: Int) ->{cap2} Int)^{}


Why is there additional empty cs added to the function type?

tests/neg-custom-args/captures/extending-cap-classes.scala

A maximal capability is one that derives from `caps.Cap`. Also: drop the given caps.Cap. It's not clear why there needs to be a given for it.

The current handling of class type refinements is unsound. We cannot simply use a variable for the capture set of a class argument. What we need to do instead is treat class arguments as tracked. In this commit we at least allow explicitly declared tracked arguments. This needed two modifications: - Don't additionally add a capture set for tracked arguments - Handle the case where a capture reference is of a singleton type which is another capture reference. As a next step we should treat all class arguments as implicitly tracked.

Replace with references that inherit trait `Capability`.

Drop convention that classes inheriting from universal capturing types are capability classes. Capture sets of parents are instead ignored. The convention led to algebraic anomalies. For instance if class C extends A => B, Serializable then C <: (A => B) & Serializable, which has an empty capture set. Yet we treat every occurrence of C as implicitly carrying `cap`.

Only enrich classes with capture refinements for a parameter if the deep capture set of the parameter's type is nonempty.

… adaptation This change lets more ref trees with underlying function types keep their singleton types.

- Avoid creating capture sets of untrackable references - Refine disallowRootCapability to consider only explicit captures

When an expression has a type that derives from caps.Capability, add an explicit capture set. Also: Address other review comments

noti0na1 · 2024-05-28T14:19:01Z

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

  extension (x: CaptureRef)
     private def subsumes(y: CaptureRef)(using Context): Boolean =
      (x eq y)
      || x.isRootCapability
      || y.match
-          case y: TermRef => y.prefix eq x
+          case y: TermRef =>
+            (y.prefix eq x)
+            || y.info.match
+                case y1: CaptureRef => x.subsumes(y1)
+                case _ => false
          case MaybeCapability(y1) => x.stripMaybe.subsumes(y1)
          case _ => false
      || x.match
          case ReachCapability(x1) => x1.subsumes(y.stripReach)
+          case x: TermRef =>
+            x.info match
+              case x1: CaptureRef => x1.subsumes(y)
+              case _ => false
          case _ => false


A version supporting more general TermRefs:

extension (x: CaptureRef) private def subsumes(y: Type)(using Context): Boolean = (x eq y) || x.isRootCapability || y.match case y: TermRef => // Change eq to subsumes in the future for supporting path as elements (y.prefix eq x) || x.subsumes(y.info) case y: AndType => x.subsumes(y.tp1) || x.subsumes(y.tp2) case y: OrType => x.subsumes(y.tp1) && x.subsumes(y.tp2) case CapturingType(y1, refs) => x.subsumes(y1) && refs.accountsFor(x) case MaybeCapability(y1) => x.stripMaybe.subsumes(y1) case _ => false || x.match case ReachCapability(x1) => y.match case y: CaptureRef => x1.subsumes(y.stripReach) case _ => false case _ => false

The case for underlying type of TermRef x should be covered by accountsFor.

Let's discuss this change in another PR.

propensive reviewed May 13, 2024

View reviewed changes

odersky requested a review from noti0na1 May 19, 2024 11:24

odersky assigned noti0na1 May 19, 2024

odersky requested a review from Linyxus May 19, 2024 11:24

noti0na1 requested changes May 22, 2024

View reviewed changes

odersky force-pushed the add-max-captureref branch from 2d75aaa to e801dcd Compare May 26, 2024 14:22

odersky added 10 commits May 27, 2024 16:43

Distinguish maximal from root capabilities

0268185

A maximal capability is one that derives from `caps.Cap`. Also: drop the given caps.Cap. It's not clear why there needs to be a given for it.

Drop @capability annotations

b76bc3e

Replace with references that inherit trait `Capability`.

Add fewer parameter refinements.

08557a1

Only enrich classes with capture refinements for a parameter if the deep capture set of the parameter's type is nonempty.

Drop ResetPrivate flag

f02b5fb

Turn nested environment capture sets into constants at the end of box…

0177576

… adaptation This change lets more ref trees with underlying function types keep their singleton types.

Two fixes to make tests pass as before

4487eeb

- Avoid creating capture sets of untrackable references - Refine disallowRootCapability to consider only explicit captures

Add assertions that all references in capture sets are trackable

999be5e

Make capture sets of expressions deriving Capability explicit

81cf8d8

When an expression has a type that derives from caps.Capability, add an explicit capture set. Also: Address other review comments

odersky force-pushed the add-max-captureref branch from e801dcd to 81cf8d8 Compare May 27, 2024 14:44

odersky mentioned this pull request May 27, 2024

Existential capabilities design draft #20470

Open

noti0na1 reviewed May 28, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Drop @capability annotations #20396

Drop @capability annotations #20396

odersky commented May 13, 2024

propensive May 13, 2024

odersky commented May 19, 2024 •

edited

noti0na1 left a comment

noti0na1 May 22, 2024

noti0na1 May 22, 2024

noti0na1 May 28, 2024 •

edited

odersky May 28, 2024

Drop @capability annotations #20396

Are you sure you want to change the base?

Drop @capability annotations #20396

Conversation

odersky commented May 13, 2024

propensive May 13, 2024

Choose a reason for hiding this comment

odersky commented May 19, 2024 • edited

noti0na1 left a comment

Choose a reason for hiding this comment

noti0na1 May 22, 2024

Choose a reason for hiding this comment

noti0na1 May 22, 2024

Choose a reason for hiding this comment

noti0na1 May 28, 2024 • edited

Choose a reason for hiding this comment

odersky May 28, 2024

Choose a reason for hiding this comment

odersky commented May 19, 2024 •

edited

noti0na1 May 28, 2024 •

edited