-
-
Notifications
You must be signed in to change notification settings - Fork 48
Add RFC for Recover blocks with receiver #182
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
jasoncarr0
wants to merge
10
commits into
ponylang:main
Choose a base branch
from
jasoncarr0:recover-with-receiver
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
Changes from 5 commits
Commits
Show all changes
10 commits
Select commit
Hold shift + click to select a range
89376d5
Initial commit
jasoncarr0 1295c1c
Update header
jasoncarr0 0f61c73
Add provision for consuming the target of such a recovery
jasoncarr0 6a7e65d
Update motivation with two examples of immutable expressions
jasoncarr0 96bd3c3
Apply change as -> |
jasoncarr0 b3d46a1
Update isolation and soundness conditions
jasoncarr0 80beda3
Correct accuracy of desugaring example
jasoncarr0 377a1be
Implementation doesn't need to assign cap to recover
jasoncarr0 2ddc1b1
Update teaching and unresolved questions
jasoncarr0 28a3dfc
Update syntax description
jasoncarr0 File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,153 @@ | ||
| - Feature Name: recover-with-receiver | ||
| - Start Date: 2020-08-26 | ||
| - RFC PR: (leave this empty) | ||
| - Pony Issue: (leave this empty) | ||
|
|
||
| # Summary | ||
|
|
||
| This feature will expand recover syntax to allow general usage of | ||
| recovery as appears in automatic receiver recovery. The change | ||
| will make some use cases possible, while improving the performance | ||
| or ergonomics of some other use cases. | ||
|
|
||
| # Motivation | ||
|
|
||
| Currently, Pony supports two forms of recovery, `recover` blocks, | ||
| as well as automatic receiver recovery. In some cases, these are | ||
| equivalent. If we have a single variable `x: T iso`, then we can | ||
| temporarily use it as another capability inside a recover block, | ||
| with something like: | ||
| ``` | ||
| x = recover | ||
| let x_ref = consume ref x | ||
| // do something with x ... | ||
| x_ref | ||
| end | ||
| ``` | ||
| Alternatively, if the action being taken is precisely a ref method call, | ||
| then automatic receiver recovery can be used if the | ||
| arguments and return types meet the isolation guarantees for `x`. | ||
| ``` | ||
| x.foo(y, z) | ||
| ``` | ||
| But this can't be used for every type of action, it needs to be those | ||
| actions thought of by the original class developer. We can add these methods, | ||
| but this is anti-modular. | ||
|
|
||
| This automatic receiver recovery syntax also works for expressions more complicated than a single variable of course. | ||
| The recover block is less flexible. The recover block method can be used only when the thing being modified is a mutable location. | ||
| It can be used with var fields, but not with let or embed. It can be used when we have update methods, but not with getters alone. | ||
| ``` | ||
| // defined elsehwere | ||
| class Foo | ||
| fun box getSomething(): this->Bar ref | ||
| ... | ||
| fun box values(): this->FooIterator ref | ||
|
|
||
| class FooHolder | ||
| embed foo: Foo iso = Foo | ||
| // or let | ||
|
|
||
| fun ref doSomethingWithFoo() => | ||
| // error, iso->ref = tag | ||
| foo.getSomething().somethingElse() | ||
|
|
||
| // try to recover to use foo as ref: error, can't assign | ||
| foo = recover | ||
| ... consume foo | ||
| end | ||
| end | ||
| ``` | ||
| We might also have read-only methods. Imagine we take in an Iter over iso objects. We don't want to be coupled to | ||
| the class used, such as Array, and allow a generic, potentially chained iterator. | ||
| ``` | ||
| class UsesIter[T: SomeInterface] | ||
| fun process(iter: Iterator[T]) => | ||
| // want to call a few complicated methods on T | ||
| // if T might be unique, we can't store in a variable, | ||
| // so we want to recover, but we can't! | ||
|
|
||
| // error, not a subtype | ||
| let next: T = iter.next()? | ||
|
|
||
| // ???? | ||
| iter.next() = recover | ||
| ... | ||
| end | ||
|
|
||
| // works... but only if we can | ||
| // express *all* of the things we want | ||
| // to do as multiple methods | ||
| // still anti-modular! | ||
| iter.next()?.foo().>bar() | ||
| end | ||
| ``` | ||
|
|
||
| This RFC will add a syntax to expand the design of recover blocks to allow a receiver, subsuming automatic receiver recovery. | ||
| In both cases above, the recover with receiver may be used in order to temporarily use these values as ref, allowing free | ||
| usage of methods, without requiring that the methods were defined ahead of time in the interface or class, and without | ||
| requiring extra potentially erroring accesses or allocating and swapping new values via update methods. | ||
|
|
||
| # Detailed design | ||
|
|
||
| We will add new syntactic forms to allow recover blocks based around an existing receiver expression. | ||
|
|
||
| ``` | ||
| e.recover | x => | ||
| e | ||
| end | ||
| ``` | ||
| and a shorthand | ||
| ``` | ||
| e.recover | ||
| e | ||
| end | ||
| ``` | ||
| Where in both cases, `e` is an expression, and `x` is a variable binding. In the second case, the first `e` should be either a variable or a field access. | ||
| Inside the body of the recover block, the variable `x` will be bound as a `let` binding. For the shorthand, the name of this variable will be the name | ||
| of the variable that the expression is, or the rightmost field name. | ||
|
|
||
| The capability of the new binding will depend on the capability of the expression. If it is a unique capability, `iso` or `trn`, then the resulting capability | ||
| will be the strongest aliasable type: `ref`. If it is any self-aliasing capability `k`, then the resulting capability will be `k`. | ||
| Acknowledging that there may be better choices available, at this time `iso^` or `trn^` will take the capability `ref` and act identically to their | ||
| non-ephemeral counterparts. Any variables syntactically present in the receiver expression are considered in-use for the duration of the block and cannot be consumed or re-assigned. | ||
|
|
||
| The body of the recover expression will be type-checked similarly to how recover blocks are checked today, with two exceptions. The block will have | ||
| a capability associated with it, and instead of restricting to sendable variable usage, they are restricted to capabilities which are safe-to-write. | ||
| In practice, the only special case here is writing `trn` to `trn. The result of the recover block will be adapted in the the viewpoint of the | ||
|
||
| recover block. This subsumes the existing conditions of being either unused or safe to extract. | ||
|
|
||
| If the receiver capability is not a unique cap (`iso` or `trn`), then this environment is always treated as `ref` and there are no restrictions on used or returned variables. | ||
|
|
||
| For a method call to a `ref` method, it is treated as being wrapped in an implicit receiver recovery block. That is, | ||
| `x.f(y, z)` can be de-sugared to `x.recover x.f(y, z) end`, using the shorthand syntax above. | ||
|
|
||
| For implementation, each recover block will have an optional receiver and a capability of the recover (note that this capability is different than the return capability of a regular recover block). Until the adoption of the more permissive viewpoint adaptation for ephemerals, we will have to treat recover blocks without receiver a special case. A sensible choice would be to mark all such blocks as capability `iso^`. When checking expressions for the recover block, sendability restrictions will be checked relative to the block. Return values would be checked with viewpoint adaptation as specified, except for standard recover blocks, which will use existing rules. | ||
|
|
||
| # How We Teach This | ||
|
|
||
| We can refer to this feature as either reciever recovery or recovery with receiver. The section on recover blocks will be modified with an additional section to | ||
| reflect the new type of recover blocks. In this setting we may wish to make a footnote as to `trn` receivers having looser isolation requirements. | ||
| Examples should reflect some of the previously impossible use cases above, as this helps in explaining usage of isolated capabilities in data structures. | ||
|
|
||
| The existing cases of automatic recovery, when calling ref methods, and constructors, will be presented together as conveniences. | ||
|
|
||
| # How We Test This | ||
|
|
||
| This will require additional tests for different receivers and both of the unique capabilities. Existing tests around automatic receiver recovery should be maintained and should continue to pass. | ||
|
|
||
| # Drawbacks | ||
|
|
||
| Why should we *not* do this? Things you might want to note: | ||
|
|
||
| * This may frontload recovery concepts slightly sooner for learners, rather than just presenting receiver recovery for functions | ||
| * Generic technical costs of new features | ||
|
|
||
| # Alternatives | ||
|
|
||
| We may try to expand automated recovery to handle more cases like the above, at the cost of a lack of simplicity. | ||
|
|
||
| # Unresolved questions | ||
|
|
||
| The syntax may still need work. | ||
| Research has not fully caught up to more powerful recovery mechanisms as a general detail. | ||
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is that strong enough of a restriction? Is it possible that some unsafe chicanery could be done with destructive assign to fields of an in-use variable, even if the in-use variable is not consumed?
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmmm, you're right that this wasn't written nearly as restrictive as it should be. This condition should not deviate from the soundness guaranteed by normal function calls and by recover blocks. In order to not stretch beyond what would be available to a function call, we can require that the capability be
iso^,valortag.After looking back at ponylang/ponyc#3596 I'm not convinced that the cases we gave were unsound (an
isotemporary is compatible with anisovariable in the short-term, we just need to conflate them for consumes), but that this "potentially aliases" notion is a bit more complex than just the variables which originally existed. So unless there's a very clever solution here I think we should stick with the restrictions above of requiringiso^and notisoexpressions, as by its natureiso^can never conflict with anything.Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It may not be clear what the restriction to
iso^does, it means that we cannot call any mutable methods, and hence cannot do anything else that could invalidate. We still should block consuming/assigning the variables themselves, as we would in the case of a function call (and if it is not the case that we do so, then we can log a soundness bug).