From what I’m seeing here Vale is just affine? Or am I wrong? It looks like values must be used one or zero times.
If you’ve used a language like Rust before, this might feel familiar: own-lending is semantically equivalent to borrowing a &mut Random and passing it around.
I think it’s more like this:
fn foo(value: Bar) -> Bar { value }
Rust would just ‘own’ and then return the value, like with Vale.
The --print_mem_overhead true flag is pretty sweet tbh. Wouldn’t mind that.
Not sure I understand regions yet, going to have to dig in.
Perhaps “semantically” was the wrong word choice, I meant more along the lines of architecturally equivalent, or equivalent in structure, the same way of coding minus some surface-level changes.
Re Vale’s linear types, the user generally chooses whether a type is copy (like primitives), affine, or linear. The entire stdlib and builtins are coded as if the user only ever uses linear types, and all generic variables (T in List) are assumed linear. It’s a system that allows the benefits of linear typing, and the niceties of affine types.
This is fascinating and reminds me I should try out Vale sometime. Were I voting, I would definitely vote for adding the inout syntactic sugar.
But what’s the overhead of the destructuring / restructuring needed to be able to pass a field as an owned ref? Could that exceed the cost of the skipped generation check?
I wonder if this moving in and out could actually be optimized back to a traditional &mut – just pretend that ownership goes in and out. Would make sense for a big object.
The overhead would be calling convention dependent, but if everything fits in registers, there would be no destructuring machine code left. Just load and store directly into place if they are even on the stack. The bottleneck would be the return path, as there is typically only one return register, so returning a tuple that takes more than that register would make the caller allocate an instance of the return type on the stack, and the function would get an implicit pointer argument pointing to it (that’s return value optimization). The overhead would then be to memcopy the tuple elements into place – nonzero, but not much to worry about. I presume this happens all the time when returning a Result type in Rust.
Vale always looks really interesting. I think you should write a book or something to make it easy to adopt. Last time I looked the documentation was terse.
[Rust] memory safety doesn’t come from borrow checking, not exactly. It comes from their types being affine.
Maybe my imagination is failing me, but what a borrow checker without substructural (i.e. affine/linear/ordered) types would look like? What would it check then?
Edit: I see, it’s possible to have ownership and not have borrows, you’re right. Not that a purely linear language without borrowing is practical.
From what I’m seeing here Vale is just affine? Or am I wrong? It looks like values must be used one or zero times.
I think it’s more like this:
Rust would just ‘own’ and then return the value, like with Vale.
The
--print_mem_overhead trueflag is pretty sweet tbh. Wouldn’t mind that.Not sure I understand regions yet, going to have to dig in.
Perhaps “semantically” was the wrong word choice, I meant more along the lines of architecturally equivalent, or equivalent in structure, the same way of coding minus some surface-level changes.
Re Vale’s linear types, the user generally chooses whether a type is copy (like primitives), affine, or linear. The entire stdlib and builtins are coded as if the user only ever uses linear types, and all generic variables (T in List) are assumed linear. It’s a system that allows the benefits of linear typing, and the niceties of affine types.
This is fascinating and reminds me I should try out Vale sometime. Were I voting, I would definitely vote for adding the
inoutsyntactic sugar.But what’s the overhead of the destructuring / restructuring needed to be able to pass a field as an owned ref? Could that exceed the cost of the skipped generation check?
I wonder if this moving in and out could actually be optimized back to a traditional
&mut– just pretend that ownership goes in and out. Would make sense for a big object.The overhead would be calling convention dependent, but if everything fits in registers, there would be no destructuring machine code left. Just load and store directly into place if they are even on the stack. The bottleneck would be the return path, as there is typically only one return register, so returning a tuple that takes more than that register would make the caller allocate an instance of the return type on the stack, and the function would get an implicit pointer argument pointing to it (that’s return value optimization). The overhead would then be to memcopy the tuple elements into place – nonzero, but not much to worry about. I presume this happens all the time when returning a
Resulttype in Rust.Vale always looks really interesting. I think you should write a book or something to make it easy to adopt. Last time I looked the documentation was terse.
Maybe my imagination is failing me, but what a borrow checker without substructural (i.e. affine/linear/ordered) types would look like? What would it check then?
Edit: I see, it’s possible to have ownership and not have borrows, you’re right. Not that a purely linear language without borrowing is practical.