Drop @capability annotations #20396
Open
Drop @capability annotations #20396
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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`.
propensive
reviewed
May 13, 2024
| @@ -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") | |||
There was a problem hiding this comment.
Why not phrase this as, ...let it extend the...? derives has an established meaning which isn't what's intended here.
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
|
Summary of changes:
|
noti0na1
requested changes
May 22, 2024
Comment on lines
+206
to
+208
| /** Does type derive from caps.Capability?, which means it references of this | ||
| * type are maximal capabilities? | ||
| */ |
There was a problem hiding this comment.
Checks if the type derives from `caps.Capability`, which means
references of this type are maximal capabilities.
| @@ -158,6 +159,10 @@ sealed abstract class CaptureSet extends Showable: | |||
| case _ => false | |||
| || x.match | |||
| case ReachCapability(x1) => x1.subsumes(y.stripReach) | |||
| case x: TermRef => | |||
There was a problem hiding this comment.
I think we can do similar check for TermRef y as well.
| @@ -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 ? */ | |||
There was a problem hiding this comment.
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.
| | 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)^{} |
There was a problem hiding this comment.
Why is there additional empty cs added to the function type?
|
|
||
| def test = | ||
| val x1: C1 = new C1 | ||
| val x2: C1 = new C2 // error |
There was a problem hiding this comment.
Why this test is deleted? A term with type C2 or C3 should be tracked, and not able to be assigned to a pure C1.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.