Storable leases

[crlf0710]

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, the NodeIndex and EdgeIndex is a poor man's untyped runtime version of lease.

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 a selector.(Need better names). The root part will be used for static analysis, while the selector part is stored in memory and used for runtime checking and accesses.

Introduce a new mode for places, called ScopedLeased, with surface syntax its{LeaseRootType} PlaceType, that stores LeaseSelector alongside with the value.

class Graph(
    nodes: [NodeData]
    edges: [EdgeData]
)

// Not valid Tada, borrowing surface syntax from rust.
impl LeaseBook<NodeData> for Graph {
    type Selector = usize;
    // TODO
}

impl LeaseBook<EdgeData> for Graph {
    type Selector = usize;
    // TODO
}

class NodeData(
    first_outgoing_edge: Option<its{Graph} EdgeData>
)

class EdgeData {
    target: its{Graph} NodeData,
    next_outgoing_edge: Option<its{Graph} EdgeData>
}

impl EdgeData {
     fn target(its{Graph} self) -> its{Graph} NodeData {
            self.target{root(self)} // the `root(self)` expression returns the `borrowed Graph` and we pass it along.
     }
}

Unresolved questions:

• How this fits into the uniqueness/ownership axes.
• How to deal with out-of-bound errors (the lease is previously actually retrieved from another LeaseBook, so the root and selector doesn't match)
• How to prevent unsafety. eg. Incorrectly specifying unpinned-pointers as Selector.

[lqd]

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.

[crlf0710]

@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".

[nikomatsakis]

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).