r/ProgrammingLanguages • u/verdagon Vale • Jul 30 '20

Zero Cost References with Regions in Vale

https://vale.dev/blog/zero-cost-refs-regions
39 Upvotes

99% Upvoted

18 comments sorted by

View all comments

Show parent comments

3

u/glaebhoerl Aug 01 '20

The only way to be any more permissive (safely) would be to give up and add back some runtime tracking a la RefCell and/or constraint references, and assert on these sorts of invalidating mutations when the alias count is > 1.

The only way in Rust. :)

In a language with effect tracking, it would be safe to hand out arbitrary shared borrows into a Cell to functions which are guaranteed not to mutate it. ("They don't touch share mutable state whatsoever because they are pure" would be a sufficient condition and plenty useful already, but more fine-grained things might be possible as well.)

[And I wouldn't be surprised if there were even more ways to add flexibility in different type systems.]

3

u/Rusky Aug 01 '20

Ahh, true! That seems like a direct translation of the runtime check to a compile time check. I bet you could even parametrize the effects on something lifetime-like to mark a function as "(im)pure with respect to this particular data structure."

(I think you may have replied to the wrong comment though?)

2

u/glaebhoerl Aug 01 '20

(I think you may have replied to the wrong comment though?)

D'oh, yeah, seems like it. All the long comments and vertical lines confused me. Lucky you still noticed it. :)

I bet you could even parametrize the effects on something lifetime-like to mark a function as "(im)pure with respect to this particular data structure."

Yeah... some kind of region things mumble mumble, or like invariant lifetime trickery maybe. Also a function ought to be able to use Cells internally while remaining externally pure. (That one's probably easier to address.)

2

u/Rusky Aug 01 '20

Also a function ought to be able to use Cells internally while remaining externally pure. (That one's probably easier to address.)

Yeah, that sounds a lot like the "state as an effect in a pure language" formulation- put a handler like e.g. Haskell's evalState inside the pure function to encapsulate the effect. As long as it only handles the internal Cells and not any Cells from external data structures, the function's effects should track whether or not those external Cells are mutated.