From 89376d5519342f0f904a362961fa2940c7cc8e9a Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Wed, 26 Aug 2020 19:52:22 -0700 Subject: [PATCH 01/10] Initial commit --- text/0000-recover-with-receiver.md | 101 +++++++++++++++++++++++++++++ 1 file changed, 101 insertions(+) create mode 100644 text/0000-recover-with-receiver.md diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md new file mode 100644 index 00000000..9b74edbb --- /dev/null +++ b/text/0000-recover-with-receiver.md @@ -0,0 +1,101 @@ +- Feature Name: (fill me in with a unique ident, my_awesome_feature) +- Start Date: (fill me in with today's date, YYYY-MM-DD) +- 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) +``` + +This automatic receiver recovery syntax also works for expressions more complicated than a single variable, but the above recover block method may be cumbersome such as `obj.field` when `field` is a var, or impossible, such as for `obj.field` with a let, or `array(i)?` when an array has `iso` entries. +In these cases, only existing methods may be called, greatly restricting usage. + +This RFC will add a syntax to expand the design of recover blocks to allow a receiver, subsuming automatic receiver recovery. + +# Detailed design + +We will add new syntactic forms to allow recover blocks based around an existing receiver expression. + +``` +e.recover as 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. + +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. From 1295c1c4988d7174ebdb17c9c972f5b1220b8d8f Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Wed, 26 Aug 2020 19:54:12 -0700 Subject: [PATCH 02/10] Update header --- text/0000-recover-with-receiver.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md index 9b74edbb..036d02d5 100644 --- a/text/0000-recover-with-receiver.md +++ b/text/0000-recover-with-receiver.md @@ -1,5 +1,5 @@ -- Feature Name: (fill me in with a unique ident, my_awesome_feature) -- Start Date: (fill me in with today's date, YYYY-MM-DD) +- Feature Name: recover-with-receiver +- Start Date: 2020-08-26 - RFC PR: (leave this empty) - Pony Issue: (leave this empty) From 0f61c738c94ce9f08432e6432b203c2b942fadc3 Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Wed, 26 Aug 2020 20:07:00 -0700 Subject: [PATCH 03/10] Add provision for consuming the target of such a recovery --- text/0000-recover-with-receiver.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md index 036d02d5..2f1fba3c 100644 --- a/text/0000-recover-with-receiver.md +++ b/text/0000-recover-with-receiver.md @@ -58,7 +58,7 @@ 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. +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. From 6a7e65d24e511d6dd28693492f10072e8697d190 Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Thu, 27 Aug 2020 06:39:00 -0700 Subject: [PATCH 04/10] Update motivation with two examples of immutable expressions --- text/0000-recover-with-receiver.md | 56 ++++++++++++++++++++++++++++-- 1 file changed, 54 insertions(+), 2 deletions(-) diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md index 2f1fba3c..368624b6 100644 --- a/text/0000-recover-with-receiver.md +++ b/text/0000-recover-with-receiver.md @@ -30,11 +30,63 @@ 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, but the above recover block method may be cumbersome such as `obj.field` when `field` is a var, or impossible, such as for `obj.field` with a let, or `array(i)?` when an array has `iso` entries. -In these cases, only existing methods may be called, greatly restricting usage. +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 From 96bd3c355d9747dec3b2c1d5e38951c4e8934f62 Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Tue, 8 Sep 2020 16:57:59 -0700 Subject: [PATCH 05/10] Apply change as -> | --- text/0000-recover-with-receiver.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md index 368624b6..1194a957 100644 --- a/text/0000-recover-with-receiver.md +++ b/text/0000-recover-with-receiver.md @@ -93,7 +93,7 @@ requiring extra potentially erroring accesses or allocating and swapping new val We will add new syntactic forms to allow recover blocks based around an existing receiver expression. ``` -e.recover as x => +e.recover | x => e end ``` From b3d46a12fb7216742c0d19a431245519066f288c Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Sat, 12 Sep 2020 11:09:45 -0700 Subject: [PATCH 06/10] Update isolation and soundness conditions --- text/0000-recover-with-receiver.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md index 1194a957..5eaa9386 100644 --- a/text/0000-recover-with-receiver.md +++ b/text/0000-recover-with-receiver.md @@ -109,15 +109,16 @@ 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. +Acknowledging that there might be better choices available, at this time `iso^` or `trn^` will take the capability `ref` and act identically to their +non-ephemeral counterparts. -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. +To soundly access the outside environment, we must use a few provisions: +* As in any recover block, the outside environment can be accessed only via sendables +* All variables which were used in the receiver of the block are considered in-use (and cannot be consumed) +* To prevent invalidation, the outside environment should be accessed only immutably (though this condition can be loosened for provably disjoint references). + This does not prevent consuming `iso` variables to move into the recover block, as they are always disjoint from the receiver. -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. +The value which is returned will be viewpoint-adapted according to the capability of the receiver. This subsumes the existing conditions for the returns of automatic receiver recovery. 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. From 80beda39212412558736ab32984b1865b04aebc3 Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Sat, 12 Sep 2020 11:10:05 -0700 Subject: [PATCH 07/10] Correct accuracy of desugaring example --- text/0000-recover-with-receiver.md | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md index 5eaa9386..a876ca19 100644 --- a/text/0000-recover-with-receiver.md +++ b/text/0000-recover-with-receiver.md @@ -120,8 +120,17 @@ To soundly access the outside environment, we must use a few provisions: The value which is returned will be viewpoint-adapted according to the capability of the receiver. This subsumes the existing conditions for the returns of automatic receiver recovery. -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 a method call to a `ref` method, it can be treated as being wrapped in an implicit receiver recovery block. That is, +`x.f(y, z)` can be de-sugared to: +``` +let a1 = y +let a2 = z +x.recover + x.f(consume a1, consume a2) +end +``` +Note that the arguments are evaluated ahead of time, and then consumed. This is how automatic receiver recovery prevents invalidation today, by allowing +no execution to take place after the receiver has been determined. 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. From 377a1bef7cb4aaa5940021e8b7dbae78120a6465 Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Sat, 12 Sep 2020 11:10:39 -0700 Subject: [PATCH 08/10] Implementation doesn't need to assign cap to recover --- text/0000-recover-with-receiver.md | 1 - 1 file changed, 1 deletion(-) diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md index a876ca19..e61bbbea 100644 --- a/text/0000-recover-with-receiver.md +++ b/text/0000-recover-with-receiver.md @@ -132,7 +132,6 @@ end Note that the arguments are evaluated ahead of time, and then consumed. This is how automatic receiver recovery prevents invalidation today, by allowing no execution to take place after the receiver has been determined. -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 From 2ddc1b1075eac9fccd08b5af7eaaa6faa05a87e3 Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Sat, 12 Sep 2020 11:10:53 -0700 Subject: [PATCH 09/10] Update teaching and unresolved questions --- text/0000-recover-with-receiver.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md index e61bbbea..b1703432 100644 --- a/text/0000-recover-with-receiver.md +++ b/text/0000-recover-with-receiver.md @@ -136,10 +136,10 @@ no execution to take place after the receiver has been determined. # 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. +reflect the new type of recover blocks. 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. +The existing cases of automatic recovery, when calling ref methods, and constructors, will be presented together as conveniences, as it is now a truly representable +form of recovery. # How We Test This @@ -158,5 +158,6 @@ We may try to expand automated recovery to handle more cases like the above, at # Unresolved questions -The syntax may still need work. -Research has not fully caught up to more powerful recovery mechanisms as a general detail. +* The syntax may still need work. +* Research has not fully caught up to more powerful recovery mechanisms as a general detail. +* Some methods may be given more flexible types, but these can't be easily expressed generically. Should we add new connectives? From 28a3dfc9ee72c8d273ab0c1e201b72e8b254c642 Mon Sep 17 00:00:00 2001 From: Jason Carr Date: Sat, 12 Sep 2020 11:12:30 -0700 Subject: [PATCH 10/10] Update syntax description --- text/0000-recover-with-receiver.md | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/text/0000-recover-with-receiver.md b/text/0000-recover-with-receiver.md index b1703432..dc0a3085 100644 --- a/text/0000-recover-with-receiver.md +++ b/text/0000-recover-with-receiver.md @@ -93,16 +93,23 @@ requiring extra potentially erroring accesses or allocating and swapping new val We will add new syntactic forms to allow recover blocks based around an existing receiver expression. ``` -e.recover | x => - e +e1.recover | x => + e2[x] end ``` -and a shorthand +and shorthands ``` -e.recover - e +x.recover + e[x] end ``` +and shorthands +``` +x.f.recover + e[f] +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.