Merged
Conversation
propensive
reviewed
May 13, 2024
| */ | ||
| @experimental final class capability extends StaticAnnotation | ||
| @experimental | ||
| @deprecated("To make a class a capability, let it derive from the `Capability` trait instead") |
Contributor
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.
Contributor
Author
|
Summary of changes:
|
noti0na1
requested changes
May 22, 2024
Member
noti0na1
left a comment
There was a problem hiding this comment.
There are still some import of annotation.capability can be deleted; the document should be updated as well.
| | ^ | ||
| | Found: (x$0: Int) ->{cap2} Int | ||
| | Required: (x$0: Int) -> Int | ||
| | Found: ((x$0: Int) ->{cap2} Int)^{} |
Member
There was a problem hiding this comment.
Why is there additional empty cs added to the function type?
2d75aaa to
e801dcd
Compare
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
e801dcd to
81cf8d8
Compare
noti0na1
reviewed
May 28, 2024
This file contains hidden or 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
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.