Surprised there's no mention of Austral[1] in related work. Austral has read and write borrows for linear types, and has been around for a few years.
It uses special `Region` types for borrows, where a linear type `Foo` is wrapped in a reference of type `ReadReference[Foo, R]` or `WriteReference[Foo, R]` (abbreviated as `&[Foo, R]` and `&![Foo, R]` respectively), for some region `R`. The reference takes ownership of the value.
The borrow statement creates a lexical block with a Region type, and within the region the borrowed value is of the reference type tied to that region.
type Foo : Linear
let foo : Foo = ...
borrow foo as foo_ref in SomeRegion do -- SomeRegion has no prior definition. It is defined here.
-- cannot access `foo` in this region as it has been borrowed and is owned by `foo_ref`.
-- foo_ref has type &[Foo, SomeRegion]
end; -- foo_ref cannot escape this region
-- since `SomeRegion` no longer exists.
-- foo_ref gives up ownership of the value and it returns to `foo`.
-- Can access `foo` again here as it is no longer borrowed.
For mutable borrows the syntax is the same except the keyword `borrow!` is used instead.
borrow! foo as foo_ref in SomeRegion do
-- foo_ref has type &![Foo, SomeRegion]
end;
In addition to the borrow statement, we can associate a region with a full function by making it region generic.
generic [SomeRegion: Region]
function some_reader(&[Foo, SomeRegion]) : T;
generic [SomeRegion: Region]
function some_writer(&![Foo, SomeRegion]) : Unit;
Then we can use the more terse prefix borrow expression, which creates an anonymous region and wraps its argument in a reference using that region, so calls to these functions are just:
some_reader(&foo);
some_writer(&!foo);
Instead of having to write out the more verbose statement form with explicit regions:
borrow foo as foo_ref in SomeRegion do
some_reader(foo_ref);
end;
borrow! foo as foo_ref in SomeRegion do
some_writer(foo_ref);
end;
Surprised there's no mention of Austral[1] in related work. Austral has read and write borrows for linear types, and has been around for a few years.
It uses special `Region` types for borrows, where a linear type `Foo` is wrapped in a reference of type `ReadReference[Foo, R]` or `WriteReference[Foo, R]` (abbreviated as `&[Foo, R]` and `&![Foo, R]` respectively), for some region `R`. The reference takes ownership of the value.
The borrow statement creates a lexical block with a Region type, and within the region the borrowed value is of the reference type tied to that region.
For mutable borrows the syntax is the same except the keyword `borrow!` is used instead. In addition to the borrow statement, we can associate a region with a full function by making it region generic. Then we can use the more terse prefix borrow expression, which creates an anonymous region and wraps its argument in a reference using that region, so calls to these functions are just: Instead of having to write out the more verbose statement form with explicit regions: [1]:https://austral-lang.org/tutorial/borrowing