Functional ownership through fractional uniqueness

by matt_d • 2 years ago

122 49 2 years ago

$Preview of Functional ownership through fractional uniqueness$ arxiv.org

    the Rust compiler is able to infer that allowing two mutable borrows 
    is safe as long as one of them is never used

This (i.e. proving a variable is never used) is impossible in general since it is equivalent to the halting problem. There are many cases where it can be solved, so the compiler lets the programmer get away with this in the cases where one of the mutable borrows is provably not used. Now imagine re-factoring the code so that the compiler could no longer produce the proof. Now an error is generated and the programmer is left scratching their head wondering where this new error came from.

nh23423fefe• 2 years ago

why is it a head scratcher? the error message seems clear?

waynecochran5• 2 years ago

The head scratcher is that as soon as the compiler can't produce the proof (even though the borrow still may be unreachable) an error is generated. The programmer will be wondering why a new error cropped up when they may not have been doing anything that was semantically any different.

parentheses• 2 years ago

compiler != runtime

ultimately no code is free of side effects. this is a tool to mark code as safe and propagate that safety up the call stack to make your code's safety something you can reason about.

it's definitely true that if a piece of code is unsafe, you need to be more careful.

(not a rust programmer, but have had to fight the compiler when i first looked at it)

waynecochran5• 2 years ago

This is a static error. A compiler generated error. With static analysis reachability is not computable.

Rusky2• 2 years ago

The compiler doesn't do anything here that is hard to understand- its approximate solution works purely in terms of the control flow graph, so there is a very clear and bright dividing line between "you have a use of this variable here" and not, which is never impacted by anything subtle about the values of conditions or whatever.

The closest to head-scratching that I have ever seen here are the sorts of errors that include "note: value may be accessed in another iteration of this loop," or perhaps the corner cases that Polonius aims to solve if you count those.

layer82• 2 years ago

In an ideal (?) world, a refactoring would come along with a machine proof that the refactored code is equivalent to the original code (because otherwise, how can you be sure?). In that case, the compiler would also be able to prove that the code is still safe.

I believe that type checking should closely match the reasoning programmers do in their head, and thereby verify the correctness of that reasoning. Conversely, this means that programmers must express their reasoning through the type system. If something doesn’t typecheck, either the reasoning as expressed is wrong or incomplete, or the programmer has used some reasoning that cannot be expressed in the type system (meaning that the type system is lacking in that respect).

waynecochran5• 2 years ago

Proving that two programs are the same is not decidable either.

lmm5• 2 years ago

I believe that type checking should closely match the reasoning programmers do in their head, and thereby verify the correctness of that reasoning. Conversely, this means that programmers must express their reasoning through the type system. If something doesn’t typecheck, either the reasoning as expressed is wrong or incomplete, or the programmer has used some reasoning that cannot be expressed in the type system (meaning that the type system is lacking in that respect).

Right. The (well, a) problem with NLL in Rust is that it isn't expressible; it creates lifetimes that don't correspond to anything in the syntax, and so can't be written explicitly into the program even if the programmer wants to. (As opposed to conventional type inference where you can always write the type explicitly if the code is confusing)

Hugsun2• 2 years ago

The quote betrays a slight misunderstanding of non lexical lifetimes. The two borrows happen in separate implicit scopes. The first borrow is only valid until the second borrow is made. At that point it's dropped. So the two mutable references can't exist at the same time.

A refactor that breaks this ordering results in code that obviously shouldn't work in the eyes of any non-beginner rust programmer.

legerdemain4• 2 years ago

You can 100% have multiple mutable references to the same variable in the same scope, without the first one getting dropped. For example:

   fn main() {
      let mut s = String::from("s");
      let mut1: &mut _ = &mut s;
      let mut2: &mut _ = &mut *mut1;
      *mut2 = String::from("t");
      println!("using mut2: {mut2}");
      println!("using mut1: {mut1}");
   }

Some people use a mental model of reference lifetimes that allows "discontinuous lifetimes" where the valid region has holes. I don't think that's how the compiler models reborrowing, and even under that model, `mut1` is created before `mut2` and gets dropped after `mut2`.

lmm5• 2 years ago

Yeah. This is why I think NLL is a mistake, just as I've come to think that implicit TCE is a mistake. Our tools must not only be correct but also comprehensible.

throwaway17_176• 2 years ago

Do you mean Tail Call Elimination? If so, are you thinking of all tail calls, or are you more focusing on the conversion of recursive calls to iteration?

SkiFire132• 2 years ago

NLL resemble how many people reason about lifetimes. Without them you would have to introduce scopes everywhere for no gain (and also, even before NLL stuff like method calls was special cased to work kinda like NLL does today, otherwise it would have been an utter pain)

SkiFire132• 2 years ago

The statement "proving a variable is never used" is not fully specified. What does it mean for it to not be used? (Or rather, not be used again?). One way to interpret it (which I think is the one you used) is that at runtime it will no longer be read/wrote. Another one is to that it is no longer syntactically referenced, which is much easier to reason about and statically prove.

digdugdirk• 2 years ago

What're some good resources to build up the knowledge base needed to understand this article?

I've always been fascinated by the building blocks of computation, there just seems to be a massive investment required to get that understanding.

ChadNauseam• 2 years ago

A while back I interviewed a coauthor of this paper here: https://www.youtube.com/watch?v=rqArTpY_kNY

We discussed the language he's helping develop (Granule) and which the concepts in this paper are implemented in. I actually asked him if he thought something like this paper would be possible and IIRC he said he was hopeful. I think listening to the interview would be a good way to get a feel for the big ideas.

To get deeper into it, I'd recommend learning Haskell at least up to the point where you understand typeclasses, functors, and monads. That will get you familiar with some relatively advanced type system features. Granule is a research language so it has additional stuff going on, but that is a solid foundation. After that, just google terms you don't know (e.g. modal type theory) or look at the papers that are cited. You can also join the PLTD discord server, there are lots of type nerds in there who are usually happy to answer questions.

matt_d• 2 years ago

I'd recommend by starting with the talk by Daniel Marshall (one of the authors) from Lambda Days 2023, "A Hitchhiker's Guide to Linearity", https://www.youtube.com/watch?v=QtlkqJGdnuM

The Granule Project's website, https://granule-project.github.io/, links relevant resources, too, in particular https://granule-project.github.io/granule.html and https://github.com/granule-project/granule/blob/main/example...

The latter tutorial is based on "Quantitative program reasoning with graded modal types" (ICFP 2019), with the talk and paper available at https://dl.acm.org/doi/10.1145/3341714

See also "Linearity and Uniqueness: An Entente Cordiale" (ESOP 2022), https://granule-project.github.io/papers/esop22-paper.pdf

throwaway17_176• 2 years ago

The work done in the Gradle project by Orchard, et al has been consistently good. I think a really solid progression from this paper is to take the same approach and combine it with the type system feature in ‘A Flexible Type System for Fearless Concurrency’ (Milano,etal 2022) [1]. The thrust of said paper is to utilize a coarser grain for ‘objects’ than what Rust promotes, which allows for much simpler implementations of common data structures (the paper uses a doubly linked, circular list as a well worked out example). Combining Milano’s approach to the scale at which ‘ownership’ is applied with the graded modality work from Orchard, et al would produce a very promising type system, with less syntactic noise from annotations, and still allow for a sliding scale of fineness in ownership semantics.

1 - https://dl.acm.org/doi/pdf/10.1145/3519939.3523443

carterschonwald2• 2 years ago

I think you mean Granule

throwaway17_176• 2 years ago

True, Granule and Gerty are the language implementations out of Orchard’s group. Thanks for the correction.

riscy• 2 years ago

Swift recently adopted a region-based approach for safe concurrency that builds on Milano et al’s ideas (shared co-author as well): https://github.com/apple/swift-evolution/blob/main/proposals...

throwaway17_176• 2 years ago

I didn’t know it had gotten approved/merged. She (Milano) gave a talk at Strange Loop in ~October of 2023 and reviewed her research work and mentioned on one of the last few slides there was a formal proposal for the implementing the system in Swift. I bookmarked it earlier today, now I’ll have to find the whole discussion history and read that too.

carterschonwald2• 2 years ago

I recently read this series of papers, and while I don’t like the exact specific APIs they cook up, the core insights are wonderful.

The fractional piece of a generated symbol / variable is a really nice way to think about may-alias information.

Likewise the way they talk about uniqueness as aliasing info from the past and linearity as aliasing info for the future, in the precursor paper, is a really nice explanation, that while being per se folk lore, is really hard to remember or explain usually.

trinsic2• 2 years ago

Can anyone give me a example of of what this could be compared to in the world? As a non-programmar Im having trouble understanding what this is and how this is important, but the headline sounds interesting.

Functional ownership through fractional uniqueness

Related Stories