4 ms·

From Linear Types to Borrowing

5 points by fanf2 1y ago

sparkie 1y ago
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; [1]:https://austral-lang.org/tutorial/borrowing https://austral-lang.org/tutorial/borrowing

5 points by fanf2 1y ago

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; [1]:https://austral-lang.org/tutorial/borrowing https://austral-lang.org/tutorial/borrowing