Open crlf0710 opened 2 years ago
Have either of you looked at @cfallin's work on "Deferred borrows" btw ? https://cfallin.org/pubs/ecoop2020_defborrow.pdf
My recollection is that "path-dependent types" didn't seem completely necessary (especially modeling lifetimes as oxide/polonius-style origins, and therefore, IIUC, as dada leases) but I could have misunderstood.
The deferred borrows themselves looked more closely related to the same problem as the OP, and why I mention them.
@lqd Thanks for the pointer, i gave it a read after you posted the link. Yes, the work is based-on the status quo of the rust language, useful in certain situations, and suffers from exactly the same issue (borrow has to be temporary) as i wrote in the OP. I think we still cannot model graph or double-linked-list ownership ergonomically using this deferred borrows construct, given that it still carries the original lifetime.
The naive proposal above is about syntax-sugarize parts of the problem, by storing selectors (i thought it's called lens in Haskell, though i'm not very sure) as part of the "place" modes, now that type is decoupled from representation or layout in dada.(As just an example, this naive proposal will suffer from the root-selector mismatch problem, i think) But anyway, from language design level, there might be chance to fundamentally improve the situation of "long-term borrowship".
This is very interesting. I don't quite understand your example @crlf0710 but I'll give it a more careful read later, along with that paper. I'm vaguely reminded of my thesis work, actually, where I had something like Rust lifetimes but they were also runtime values (so you parameterized types by paths, naming the value).
Thank you for your very interesting work!
One thing i really really wish to be taken into consideration, is runtime-storable versions of
lease
, aka, "non-temporary lifetime".Currently rust lifetime has been doing quite well at inter-procedure ownership/borrowing relations. However most non-arena and non-static lifetimes occur with temporaries. It does not work so well when expressing data structures and business domain objects, where the ownership has to be stored.
Storable leases
Personally i think with a runtime-storable and usable version of
lease
, these issues can be eased or maybe even solved.I'd like to take your
Modeling graphs in Rust using vector indices
blog as an example, theNodeIndex
andEdgeIndex
is a poor man's untyped runtime version oflease
.I believe allowing some (even restricted) version of runtime lease will fundamentally improve the ergonomics of writing a graph.
POC naive proposal without deep thinking
A runtime lease consists of two parts: a
root
and aselector
.(Need better names). Theroot
part will be used for static analysis, while theselector
part is stored in memory and used for runtime checking and accesses.Introduce a new mode for places, called
ScopedLeased
, with surface syntaxits{LeaseRootType} PlaceType
, that storesLeaseSelector
alongside with the value.Unresolved questions:
uniqueness/ownership
axes.lease
is previously actually retrieved from anotherLeaseBook
, so the root and selector doesn't match)Selector
.