You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
TL;DR: Explanation of the issue with extracting fields from a consumed reference, and initial proposal of a syntax
When handling viewpoint adaptation field extraction (especially with iso origins), there is no way to safely extract multiple let fields, or extracting var fields without reallocating them. Examples:
classFoolet x: Stringisolet y: Stringisonewisocreate(x': Stringiso, y': Stringiso) =>
x = consume x'; y = consume y'
classBarvar x: Stringisovar y: Stringisonewisocreate(x': Stringiso, y': Stringiso) =>
x = consume x'; y = consume y'
classBazlet arr: Array[Stringiso]
newisocreate(x': Stringiso, y': Stringiso) =>
arr = [consume x'; consume y']
classQuxlet tup: (Stringiso, Stringiso) // or "var tup: ..."newisocreate(x': Stringiso, y': Stringiso) =>
tup = (consume x', consume y')
actorMainvar _x: Stringiso = recoverStringendvar _y: Stringiso = recoverStringendnewcreate(env: Env) =>
let x = "x"; let y = "y"let foo: Fooiso = Foo(x.clone(), y.clone())
let bar: Bariso = Bar(x.clone(), y.clone())
let baz: Baziso = Baz(x.clone(), y.clone())
let qux: Quxiso = Qux(x.clone(), y.clone())
// Doesn't work, since you can only pick one field
_x = (consume foo).x//_y = (consume foo).y // "can't use a consumed local in an expression"// Works, but only for `var` and requires potentially unnecessary allocations
_x = bar.x = recoverStringend; _y = bar.y = recoverStringend// Works, but has runtime issues and requires an error blocktrylet baz': Baz = consume baz
_x = baz'.arr.shift()?
_y = baz'.arr.shift()?
end// Works, but data needs to be in a well-specified tuple
(_x, _y) = (consume qux).tup
The solution in Qux seems to be the best way to do this currently, but it is still error-prone if the elements are incorrectly rearranged (which is less likely to be the case for fields with different types), and it can get complicated if the receiver needs to read a few fields of a huge tuple.
I specifically mentioned viewpoint adaptation earlier as this should be valid for other reference capabilities, but iso and maybe trn origins would be the most relevant cases.
I would expect something like this to work, but it violates capabilities as expected:
// Error: iso! is not a subcap of iso
(_x, _y) = recoverlet foo': Fooref = consume foo
(foo'.x, foo'.y)
end
And consuming from fields directly is not allowed, either:
// Error: Consume expressions must specify a single identifier
_x = consume (foo.x); _y = consume (foo.y)
Some sort of syntax that "consumes a reference and returns a tuple of its fields, specified by the programmer" would make sense to respect capabilities. For now, I thought of a "destructor" (as in the reverse of a constructor, or the de-structuring of the origin object) syntax:
When checking refcaps, if foo is of type Any A, foo' would be Any A^ in both tuple calls.
As far as I can tell, since foo' only lives inside the "destruct" block, no other refcaps could leak, so long as no other values, fields or functions can exist in the rightside (tuple expression) of the block. Alternatively, foo' isn't necessary for purposes other than readability. Some alternative syntaxes:
(_x, _y) = destruct (_ = consume foo) (_.x, _.y) end
(_x, _y) = destruct (consume foo) (x, y) end
(_x, _y) = destruct (consume foo) (.x, .y) end
(_x, _y) = destruct (consume foo) (_.x, _.y) end// etc.
Do note that consume keyword should still be used, as we might not need to consume our original variable when working with refcaps that alias as themselves -- in which case, the syntax is not necessary at all outside of generics.
I'll turn this into a PR if nobody makes a mention about this being unsound, or proposes a better syntax.
The text was updated successfully, but these errors were encountered:
TL;DR: Explanation of the issue with extracting fields from a consumed reference, and initial proposal of a syntax
When handling viewpoint adaptation field extraction (especially with
iso
origins), there is no way to safely extract multiplelet
fields, or extractingvar
fields without reallocating them. Examples:The solution in
Qux
seems to be the best way to do this currently, but it is still error-prone if the elements are incorrectly rearranged (which is less likely to be the case for fields with different types), and it can get complicated if the receiver needs to read a few fields of a huge tuple.I specifically mentioned viewpoint adaptation earlier as this should be valid for other reference capabilities, but
iso
and maybetrn
origins would be the most relevant cases.I would expect something like this to work, but it violates capabilities as expected:
And consuming from fields directly is not allowed, either:
Some sort of syntax that "consumes a reference and returns a tuple of its fields, specified by the programmer" would make sense to respect capabilities. For now, I thought of a "destructor" (as in the reverse of a constructor, or the de-structuring of the origin object) syntax:
When checking refcaps, if
foo
is of typeAny A
,foo'
would beAny A^
in both tuple calls.As far as I can tell, since
foo'
only lives inside the "destruct" block, no other refcaps could leak, so long as no other values, fields or functions can exist in the rightside (tuple expression) of the block. Alternatively,foo'
isn't necessary for purposes other than readability. Some alternative syntaxes:Do note that
consume
keyword should still be used, as we might not need to consume our original variable when working with refcaps that alias as themselves -- in which case, the syntax is not necessary at all outside of generics.I'll turn this into a PR if nobody makes a mention about this being unsound, or proposes a better syntax.
The text was updated successfully, but these errors were encountered: