Last time I read https://verdagon.dev/blog/group-borrowing I was convinced that this approach works for simple structs + arrays where all fields are public, but would quickly become unwieldy for anything requiring "path abstraction" like a binary tree or linked list. Wildcard paths solve this complaint, neat! (I did not read the golden spike articles)
Still a little nervous about "value invalidation" TOCTTOU for how this system deals with concurrency, seems shared-xor-mutable has a leg up there, but this is looking pretty nice for the single-threaded case.
Thanks =) Another thing that will help with path abstraction is "associated groups/paths", which are like associated types but for groups/paths.
I think invalidation will work well with concurrency. The more I implement it, the more I'm discovering that invalidation and normal borrow checking are actually kind of the same thing (the difference between them lies elsewhere). So I think it'll deal with concurrency the same way as normal borrow checking. Specifically:
If someone has a reference into some data that is currently being shared to another thread via structured concurrency, they won't be able to mutate it during the structured concurrency.
If someone has a reference into some data that has been moved to another thread, they won't be able to dereference it because, well, it's been moved away.
I'm having trouble putting it all in english, but I feel like a key here is that if a function (or scope?) has no mut effects, then it's effectively taking an "immutable" reference. From that, all the normal shared-xor-mutable benefits apply.
If someone has a reference into some data that is currently being shared to another thread via structured concurrency, they won't be able to mutate it during the structured concurrency.
This is what I'm saying: that sounds eerily similar to shared-xor-mutable :P
It seems like one plan would be to:
Define closure types that have/don't have mut effects inside them
Define structured concurrency to always take closures that don't have mut effects inside them
Define mutexes which can apply closures with mut effects without also being a mut effect externally.
Do you have a sense for how your approach relates to OxCaml's Modes?
I have a hunch that Ante's safe shared mutability is built on something morally equivalent to OxCaml's uniqueness mode*. I know that group borrowing is different from Ante's approach, but they're clearly related.
I'm still excited about OxCaml, but a bit less than I used to be. Modes are elegant, but the language keeps getting more of them, and I'm afraid all the different possible combinations are going to make the language too unwieldy.
*here's a quote from the docs:
Uniqueness is irrelevant for types that don’t contain any memory locations subject to overwriting
It reminds me of what Ante calls "shape-stable," which I think is the same thing as what you're calling "type-stable."
polywolf | 8 hours ago
Last time I read https://verdagon.dev/blog/group-borrowing I was convinced that this approach works for simple structs + arrays where all fields are public, but would quickly become unwieldy for anything requiring "path abstraction" like a binary tree or linked list. Wildcard paths solve this complaint, neat! (I did not read the golden spike articles)
Still a little nervous about "value invalidation" TOCTTOU for how this system deals with concurrency, seems shared-xor-mutable has a leg up there, but this is looking pretty nice for the single-threaded case.
[OP] Verdagon | 7 hours ago
Thanks =) Another thing that will help with path abstraction is "associated groups/paths", which are like associated types but for groups/paths.
I think invalidation will work well with concurrency. The more I implement it, the more I'm discovering that invalidation and normal borrow checking are actually kind of the same thing (the difference between them lies elsewhere). So I think it'll deal with concurrency the same way as normal borrow checking. Specifically:
I'm having trouble putting it all in english, but I feel like a key here is that if a function (or scope?) has no
muteffects, then it's effectively taking an "immutable" reference. From that, all the normal shared-xor-mutable benefits apply.polywolf | 6 hours ago
This is what I'm saying: that sounds eerily similar to shared-xor-mutable :P
It seems like one plan would be to:
muteffects inside themmuteffects inside themmuteffects without also being amuteffect externally.is that about right?
[OP] Verdagon | 5 hours ago
Yep, that's exactly right, well said.
davidbalbert | an hour ago
I love this!
Do you have a sense for how your approach relates to OxCaml's Modes?
I have a hunch that Ante's safe shared mutability is built on something morally equivalent to OxCaml's uniqueness mode*. I know that group borrowing is different from Ante's approach, but they're clearly related.
I'm still excited about OxCaml, but a bit less than I used to be. Modes are elegant, but the language keeps getting more of them, and I'm afraid all the different possible combinations are going to make the language too unwieldy.
*here's a quote from the docs:
It reminds me of what Ante calls "shape-stable," which I think is the same thing as what you're calling "type-stable."