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.
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.
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)
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.
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).
Proving that two real numbers are the same is not decidable either. Despite that, there are some real numbers that we can prove are equal to each other (rarely).
Yeah I am not clever enough to come up with a baby worth throwing out. Restricted to lexical scope seems pretty reasonable. Maybe someday this will compile:
let mut viridian = Colour(52, 161, 128);
let x = &mut viridian;
let y = &mut viridian;
if find_counter_example_to_Reimann_Hypothesis {
do something with x and y
}
More like you're arguing that there is no baby in the bath you want to throw out.
Coming back to your previous comment:
> This (i.e. proving a variable is never used) is impossible in general since it is equivalent to the halting problem.
Many useful provers/programs don't suffer from the halting problem. Just because you're given a turing machine doesn't mean you can't use a subset of it with different properties.
Just to make it explicit, checking an existing proof is very decidable, given a reasonable programming language. Now getting that proof does pose some practical difficulties, but it would doubtless be built up by fairly simple proofs derived from user-supplied editing steps; a bit of a pain, but not Halting-complete.
By that logic, one could never do a refactor and be confident it didn’t change program behavior. Luckily, a program and it’s refactored version aren’t two arbitrary, unrelated programs. You can generally prove if the transformations that convert one into the other keep the semantics unchanged. Conversely, one should only ever apply transformations for which this is true.
> 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)
You couldn't write explicit lifetimes before NLL, either. (Nor does conventional type inference mean you can always write the type! This is why people who design type systems care about "principal types.")
NLL (and even moreso Polonius) brought the borrow checker closer to how programmers reason about lifetimes in their head than it was before, empirically speaking. The thing you described was a worry at the time but it never turned out to be accurate.
If there is anything about the borrow check that does match your description, it is things like "borrow splitting" and mutable reborrows, which can be done locally but are not expressible in function signatures. These problems existed long before NLL, though, and don't have anything to do with syntax or lexical scope.
> You couldn't write explicit lifetimes before NLL, either.
Well, no, but you can write scopes explicitly, and all your lifetimes correspond to scopes, by definition.
> NLL (and even moreso Polonius) brought the borrow checker closer to how programmers reason about lifetimes in their head than it was before, empirically speaking. The thing you described was a worry at the time but it never turned out to be accurate.
It worked for how some programmers reason about lifetimes in their head. Not for me. Maybe I'm the minority.
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.
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`.
I read this as mut1 and mut2 both being downgraded to shared references because they aren't used to mutate anymore. I'd imagine that's not what's actually happening though?
No - that they are both &mut _ indicates that a mutable reference is being acquired regardless of whether or not they’re used for any mutation. Possibly the compiler could automatically lower to a shared reference if it detects no mutation access locally but there may be design reasons why that’s impossible (+ you can’t have a mutable and a shared reference simultaneously anyway so downgrading to shared would still be disallowed)
> and even under that model, `mut1` is created before `mut2` and gets dropped after `mut2`
I think what you're calling "holes" are what I'd just consider to be "lazy" borrowing, where the reference doesn't really matter until the first time it's dereferenced. The only use of mut1 that happens before the end of mut2's lifetime is to assign a reference mut2 to a value that is never used. In other words, mut1 is never actually dereferenced while mut2 exists. I don't consider `&mut *` as dereferencing because it's just syntax for saying "make a new mutable reference to the same thing", which is necessary because mutable references don't implement Copy or Clone. If you instead used `let mut2 = &mut s;`, it would be abundantly clear; they don't really overlap in any way that matters because nothing would change if mut1 didn't exist at all until after mut2 no longer needed to.
I don't understand what you're saying. Are you saying that "lazy borrowing" is how the compiler works, or that it's just how you mentally model Rust for your own convenience? There is no "lazy borrowing" in the Rust compiler, as far as I know.
You can create a mutable reference `mut1`, mutate through it, create a new mutable reference `mut2`, mutate through it, then mutate through `mut1` again. Here is an example to illustrate:
fn main() {
let mut s = String::from("1"); // create value
let mut1: &mut _ = &mut s; // create a ref mut
*mut1 = String::from("2"); // write through mut1
println!("using mut1: {mut1}"); // print mut1
let mut2: &mut _ = &mut *mut1; // create a second ref mut
*mut2 = String::from("3"); // write through mut2
println!("using mut2: {mut2}"); // print mut2
*mut1 = String::from("4"); // write through mut1 again
println!("using mut1: {mut1}"); // print mut1
}
Lifetime analysis can infer shorter lifetimes for unused refs. But creating refs in the wrong order matters even if you never use them, and not all orders are valid Rust programs. Here's a very small example that doesn't compile:
fn main() {
let mut s = String::from("1");
let mut1: &mut _ = &mut s;
let mut2: &mut _ = &mut s; // never used!
println!("Using mut1: {mut1}");
}
The "lazy borrowing" was just a personal mental model, not any claim about how things are implemented under the hood. That said, I think all your examples are hinging on very specific behavior from the `Deref` and `DerefMut` traits that might not apply generally.
Looking at the generating MIR output[0] from your second example changed to use the deref syntax from the first one, it seems like the value of `mut1` is silently getting downgraded to `&[&str]` under the hood, presumably due to the fact that the rules for `Deref`[1] and `DerefMut`[1] allow the compiler to liberally substitute dereferences with calls to those trait methods, which crucially allows the compiler to change the result of dereferencing `&mut` to return a shared reference. This is actually almost exactly what was being suggested in the sibling comment here: https://news.ycombinator.com/item?id=39557697.
(edited shortly after posting to rephrase without needing to use deref operator in the in-line snippets because it messed up the italics of all of the text after like this)
Would it be easier to convince you if I replaced String with a type that doesn't implement Deref or DerefMut? I do wish you had tried it yourself, because I hope your goal is to learn something about Rust and not just to argue down someone on the Internet.
fn main() {
#[derive(Debug)]
struct X(i32);
let mut s = X(1); // create value
let mut1: &mut _ = &mut s; // create a ref mut
*mut1 = X(2); // write through mut1
println!("using mut1: {mut1:?}"); // print mut1
let mut2: &mut _ = &mut *mut1; // create a second ref mut
*mut2 = X(3); // write through mut2
println!("using mut2: {mut2:?}"); // print mut2
*mut1 = X(4); // write through mut1 again
println!("using mut1: {mut1:?}"); // print mut1
}
> Would it be easier to convince you if I replaced String with a type that doesn't implement Deref or DerefMut?
`&T` and `&mut T` implement Deref (and `&mut T` implements DerefMut) for all types[0].
> I do wish you had tried it yourself, because I hope your goal is to learn something about Rust and not just to argue down someone on the Internet.
I'm pretty confused about the sharp turn you took here. I happen to think your explanation of what's going on in the code you posted is incorrect, and if you truly are hoping that others here are trying to learn, you'd be more successful in helping them by not acting as if anyone who doesn't think you're correct is acting in bad faith. From my perspective, you completely misread what I said about Deref in my last comment and then didn't follow the advice you're giving about trying out the change I suggested with your own code because the same error occurs with the struct you define if you don't use the deref operator[1]. I'm open to the idea that I'm wrong about `Deref` being the cause of all this, but you don't really seem to be open the idea that you might be incorrect, which comes across as fairly arrogant given that you haven't really demonstrated that you understand that I'm talking about the `Deref` implementation on the _reference_, not the underlying value,.
Meanwhile, you are insisting on reasoning about Rust from first principles and making lists of links to documentation that is, at best, tangentially relevant.
For example, the fact that `&T` implements Deref is not relevant here. Applying Deref::deref to a &T returns a &T. For most intents, it's a no-op.
Very interesting, thanks for showing me. Messing with the code, it fails if you access mut1 before the mutation of mut2 because of the mutable borrow.
I did know but forget that all variables are dropped at the end of a scope, not earlier. Borrows can however last for shorter times and as this example illustrates. They can be borrowed multiple times, as long as they are returned before the parent uses their borrow.
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.
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?
Yes, tail call elimination. Conversion of recursion to iteration is the most common case, I don't really understand what you're asking by distinguishing between "all tail calls" and "the conversion of recursive calls to iteration". The point is it's a similar case where a seemingly innocuous refactor can break your program because the implicit TCE stops working.
Regarding the distinguishing between recursive tail calls and other tail calls:
The conversion of tail calls to direct jumps seems to me a simpler conversion, where refactoring would be less likely to introduce errors. The conversion of recursive calls to iteration is different, I can see how the implicit conversion could lead to much more sensitive preconditions that refactoring could cause to not be satisfied.
My initial (and rather lazily considered) reaction to the potential for breakage could be wrong, I doubt it would be worth an exhaustive testing effort to validate. I find TCE to be a conversion that is worth the potential downsides in heavily functional paradigms, but I certainly sympathize with becoming more skeptical of implicit alterations to code as written.
> The conversion of tail calls to direct jumps seems to me a simpler conversion, where refactoring would be less likely to introduce errors. The conversion of recursive calls to iteration is different, I can see how the implicit conversion could lead to much more sensitive preconditions that refactoring could cause to not be satisfied.
Isn't it the same thing? If you convert a tail call to a jump, if the place you jumped to leads back to the same line (directly or indirectly) then you've converted recursion to iteration. Iteration is ultimately implemented as jumps too.
> I doubt it would be worth an exhaustive testing effort to validate. I find TCE to be a conversion that is worth the potential downsides in heavily functional paradigms, but I certainly sympathize with becoming more skeptical of implicit alterations to code as written.
I've been bitten by it often enough to be wary. I swear I once saw a language that had an explicit keyword for tail calls (not just an annotation to error out if TCO wasn't performed, but a keyword to make a tail call and no implicit optimization), which sounded like the best solution, but I can't find it now.
Interestingly, after a relatively quick check, it seems that the tail recursive conversion is actually simpler and more predictable than in the non-recursive case. For recursive calls the stack size is always the same between the caller and callee so refactoring of the recursive function is less likely to produce errors. In the general case, where caller/callee stacks are different sizes the algorithm requires more effort and analysis to ensure the proper stack adjustments are made, and such algorithms are seemingly going to more finicky with regards to changes in either function.
This certainly seems to be one of those times when my gut instinct was just absolutely backwards, so thanks for the response which prompted me to actual check my assumptions.
I have a feeling it doesn't build on recent versions, but somebody implemented https://p3rl.org/Sub::Call::Tail for perl and I'll presumably resurrect that next time I need it.
I think for some forms of unrolling clojure's loop/recur is a neat version of a limited explicit form.
Of course, I'm difficult so what -I- really want is an explicit tail-call-modulo-cons but that would be a much more involved comment than my current caffeination levels really enable.
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)
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.
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.
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 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
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.
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.
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.
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.
52 comments
[ 2.6 ms ] story [ 102 ms ] threadultimately 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)
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.
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).
Coming back to your previous comment:
> This (i.e. proving a variable is never used) is impossible in general since it is equivalent to the halting problem.
Many useful provers/programs don't suffer from the halting problem. Just because you're given a turing machine doesn't mean you can't use a subset of it with different properties.
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)
NLL (and even moreso Polonius) brought the borrow checker closer to how programmers reason about lifetimes in their head than it was before, empirically speaking. The thing you described was a worry at the time but it never turned out to be accurate.
If there is anything about the borrow check that does match your description, it is things like "borrow splitting" and mutable reborrows, which can be done locally but are not expressible in function signatures. These problems existed long before NLL, though, and don't have anything to do with syntax or lexical scope.
Well, no, but you can write scopes explicitly, and all your lifetimes correspond to scopes, by definition.
> NLL (and even moreso Polonius) brought the borrow checker closer to how programmers reason about lifetimes in their head than it was before, empirically speaking. The thing you described was a worry at the time but it never turned out to be accurate.
It worked for how some programmers reason about lifetimes in their head. Not for me. Maybe I'm the minority.
A refactor that breaks this ordering results in code that obviously shouldn't work in the eyes of any non-beginner rust programmer.
I think what you're calling "holes" are what I'd just consider to be "lazy" borrowing, where the reference doesn't really matter until the first time it's dereferenced. The only use of mut1 that happens before the end of mut2's lifetime is to assign a reference mut2 to a value that is never used. In other words, mut1 is never actually dereferenced while mut2 exists. I don't consider `&mut *` as dereferencing because it's just syntax for saying "make a new mutable reference to the same thing", which is necessary because mutable references don't implement Copy or Clone. If you instead used `let mut2 = &mut s;`, it would be abundantly clear; they don't really overlap in any way that matters because nothing would change if mut1 didn't exist at all until after mut2 no longer needed to.
You can create a mutable reference `mut1`, mutate through it, create a new mutable reference `mut2`, mutate through it, then mutate through `mut1` again. Here is an example to illustrate:
Lifetime analysis can infer shorter lifetimes for unused refs. But creating refs in the wrong order matters even if you never use them, and not all orders are valid Rust programs. Here's a very small example that doesn't compile:Looking at the generating MIR output[0] from your second example changed to use the deref syntax from the first one, it seems like the value of `mut1` is silently getting downgraded to `&[&str]` under the hood, presumably due to the fact that the rules for `Deref`[1] and `DerefMut`[1] allow the compiler to liberally substitute dereferences with calls to those trait methods, which crucially allows the compiler to change the result of dereferencing `&mut` to return a shared reference. This is actually almost exactly what was being suggested in the sibling comment here: https://news.ycombinator.com/item?id=39557697.
[0]: https://play.rust-lang.org/?version=nightly&mode=debug&editi...
[1]: https://doc.rust-lang.org/std/ops/trait.Deref.html#deref-coe...
[2]: https://doc.rust-lang.org/std/ops/trait.DerefMut.html#mutabl...
(edited shortly after posting to rephrase without needing to use deref operator in the in-line snippets because it messed up the italics of all of the text after like this)
`&T` and `&mut T` implement Deref (and `&mut T` implements DerefMut) for all types[0].
> I do wish you had tried it yourself, because I hope your goal is to learn something about Rust and not just to argue down someone on the Internet.
I'm pretty confused about the sharp turn you took here. I happen to think your explanation of what's going on in the code you posted is incorrect, and if you truly are hoping that others here are trying to learn, you'd be more successful in helping them by not acting as if anyone who doesn't think you're correct is acting in bad faith. From my perspective, you completely misread what I said about Deref in my last comment and then didn't follow the advice you're giving about trying out the change I suggested with your own code because the same error occurs with the struct you define if you don't use the deref operator[1]. I'm open to the idea that I'm wrong about `Deref` being the cause of all this, but you don't really seem to be open the idea that you might be incorrect, which comes across as fairly arrogant given that you haven't really demonstrated that you understand that I'm talking about the `Deref` implementation on the _reference_, not the underlying value,.
[0]: https://doc.rust-lang.org/src/core/ops/deref.rs.html#164
[1]: https://play.rust-lang.org/?version=nightly&mode=debug&editi...
https://smallcultfollowing.com/babysteps/blog/2013/11/20/par...
https://haibane-tenshi.github.io/rust-reborrowing/
https://stackoverflow.com/questions/62960584/do-mutable-refe...
Meanwhile, you are insisting on reasoning about Rust from first principles and making lists of links to documentation that is, at best, tangentially relevant.
For example, the fact that `&T` implements Deref is not relevant here. Applying Deref::deref to a &T returns a &T. For most intents, it's a no-op.
I did know but forget that all variables are dropped at the end of a scope, not earlier. Borrows can however last for shorter times and as this example illustrates. They can be borrowed multiple times, as long as they are returned before the parent uses their borrow.
The conversion of tail calls to direct jumps seems to me a simpler conversion, where refactoring would be less likely to introduce errors. The conversion of recursive calls to iteration is different, I can see how the implicit conversion could lead to much more sensitive preconditions that refactoring could cause to not be satisfied.
My initial (and rather lazily considered) reaction to the potential for breakage could be wrong, I doubt it would be worth an exhaustive testing effort to validate. I find TCE to be a conversion that is worth the potential downsides in heavily functional paradigms, but I certainly sympathize with becoming more skeptical of implicit alterations to code as written.
Isn't it the same thing? If you convert a tail call to a jump, if the place you jumped to leads back to the same line (directly or indirectly) then you've converted recursion to iteration. Iteration is ultimately implemented as jumps too.
> I doubt it would be worth an exhaustive testing effort to validate. I find TCE to be a conversion that is worth the potential downsides in heavily functional paradigms, but I certainly sympathize with becoming more skeptical of implicit alterations to code as written.
I've been bitten by it often enough to be wary. I swear I once saw a language that had an explicit keyword for tail calls (not just an annotation to error out if TCO wasn't performed, but a keyword to make a tail call and no implicit optimization), which sounded like the best solution, but I can't find it now.
This certainly seems to be one of those times when my gut instinct was just absolutely backwards, so thanks for the response which prompted me to actual check my assumptions.
I think for some forms of unrolling clojure's loop/recur is a neat version of a limited explicit form.
Of course, I'm difficult so what -I- really want is an explicit tail-call-modulo-cons but that would be a much more involved comment than my current caffeination levels really enable.
I've always been fascinated by the building blocks of computation, there just seems to be a massive investment required to get that understanding.
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.
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
1 - https://dl.acm.org/doi/pdf/10.1145/3519939.3523443
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.