The Pain of Real Linear Types in Rust(gankro.github.io) |
The Pain of Real Linear Types in Rust(gankro.github.io) |
The 'dropck' pass is one of the corners of the language that has no precedent in a type system that has been proven sound (at least as far as I am aware, someone please correct me if i'm wrong), and it has had a lot of soundness issues in the past.
The fact that destructors have magical powers that the language refuses to bestow on ordinary functions is a bad sign. And destructors are terrible for predictable code: the order in which destructors run for temporary results in a single expression is not even specified by the language, and there are some surprises (https://aochagavia.github.io/blog/exploring-rusts-unspecifie...) that make it harder to write correct unsafe code.
If you were to design a language from the ground up with linear types and no destructors, it would be dramatically simpler than Rust.
I agree the system you propose would be simpler in terms of spec and effort, but I don't know about simpler to use. Much like removing mutable references in favour of `foo(X) -> X` would be a simpler type system, but awful to use compared to `foo(&mut X)`.
And Í talk from experience.
Back in the early 2000, I modified both MS VS runtime and gcc to be able to safely throw from destructors. Note to doubters that Java allows such double-exception cases and gcc already had code back then to deal with the Java case.
The way to do it is to implicitly assume that every destructor ran during stack unwinding has a try/catch surrounding it. This way, a first exception can be thrown from a destructor, but all exceptions that ultimately escape a destructor invoked during unwinding gets eaten. (Note: you can still provide your own explicit try catch in a destructor if you care about it.)
My experience with this tweak was that the horror story people come up with to reject this approach is unfounded. Here are the reasons:
1. The actual case of double-exceptions are very, very rare.
2. In the case that do arise, the second exception is often either a consequence of the first (for example, trying to access a DB were teh first exception was a failure in some DB code) or the exact same (for example running out of memory).
3. In my experience (although, since the 2nd exception is lost, I cannot actively prove this), the first exceptionis the relevant one. This is especially true due to point #2.
4. In my experience, code that care about the exact type of exception is most often either wrong or misguided. This is because such code assumes complete prescient power over what exceptions can be thrown.
5. In my experience, catching exceptions is 99% done in the top-level message or task dispatching, which doesn't care about the type of exceptions or how many occured: you just abort the operation and do some logging.
6. The fact that double exceptions are handled gracefully informs your design, which builds up and reinforce all previous points.
I once had discussion on this in the 90s in comp.lang.std.c++ and comp.lang.c++. People would not listen.
Note: to do it with STL, you do have to add try/catch within destroy() calls within containers to be able to destroy all items.
The "unsafe code" problem comes mostly from backpointers. If you have a data structure with a doubly linked list, and the forward pointer and backpointer are both pure references and can't be null, no order of destruction is strictly valid. You can't create, destroy, or manipulate a doubly linked list or a tree with backpointers in safe Rust. That's a problem.
Maybe forward pointer/backpointer pairs need to be a language level concept. The compiler needs to know that the forward pointer and the backpointer are in a relationship. The pair needs to be manipulated as a unit. You have to have mutable ownership of both references to manipulate either. The borrow checker and destructor ordering need to understand this.
If your think of your whole program as being a wrapped in an implicit State monad, holding a POSIXProcessState (e.g. exit code, registered signal handlers, file descriptors, etc.), then destructors are (POSIXProcessState -> POSIXProcessState) functions.
> You can't create, destroy, or manipulate a doubly linked list or a tree with backpointers in safe Rust. ... Maybe forward pointer/backpointer pairs need to be a language level concept.
You can define abstractions like this using unsafe code just fine. It doesn't need to be part of the language. (Think about how C++ "smart pointers" work: it's just a library.)
Destructors seem to be a
pain point
Basically explicit destructors mean the typing system needs to track lifetimes and ownership in some form or shape. There seem to be two main options.
- Simple lifetime/ownership scheme, but then you need a garbage collector anyway, and that it's mostly pointless to have explicit destructors. Just let every variable be cleaned up by the GC makes for a simpler language (under the hood clever escape analysis might be used for stack allocation of variables that don't escape their activation context).
- Avoid a GC, but then you need a complex typing system with unique owners to have any chance at expressivity (and you still need unsafe blocks and reference counting). This is Rust's choice.
Another issue is how consistently to combine destructors with other effects, in particular exceptions.
Pointer/backpointer pairs
need to be a language level
concept.
There are many more patterns where that came from, and you don't want to teach the compiler about all of them. I don't think there's anything wrong with having a lower-level "unsafe" mechanism to let you use the language itself to build new types of structures that then provide a safe interface.
As a random example, consider the rust "intrusive-collections" crate (https://crates.io/crates/intrusive-collections), which provides the kind of "no extra pointer" linked list where you can embed a list head (or multiple list heads) directly in your structure. I don't think every such crate should have its functionality native in the compiler.
EDIT: The intro has been updated to be clearer, so now I just look like an idiot. :)
arguing against
I also make it very clear that the implementation is mostly free. It's just using tools we already have with minor tweaks. Most of my issues are exactly the pragmatic matters: your standard library isn't built to handle it, nothing in the ecosystem is built to handle it, and it everyone has to opt into support for backwards compatibility reasons.
Which is exactly what they're purporting to answer...
I don't know if it's where Rust wants to be, but I want a practical-oriented ML-family language that does this.
I loop over strings a lot. Can I fit them into a nice recursive structure without runtime overhead?
Bonus round: My loops over strings often aren't straight-forward one-byte-at-a-time iterations. Sometimes my loops look at 8 or even 16 bytes in a single iteration. How does that fit in with more sophisticated types like you're describing?
Up until 2012 it was just about Linear Logic IIRC.
This ability is pretty useful when dealing with destructors that need context that you don't want to always wrap with the given type (sometimes for performance reasons).
"Must use" objects don't seem to be all that useful. More justification is needed. Is the author thinking of Javascript-like callback approaches, broken "promises", and such?
Hostility towards academia check
Anyway it's fine not to have proper linear types in Rust, but I don't think linear types are the enemy here.
"Just so you can look this stuff up in The Literature, I'll be providing all these bad names with a Trademark of Disdain™, but otherwise I'd prefer to use Rust-centric terminology." pretty clearly does.
The TM thing is obnoxious.
In theory, there's no reason one couldn't compile a linked list in source to a flat array at runtime if the access pattern was right (and linear types should make that kind of optimization a lot more practical. This might even be something one could implement "in userspace" in a language with linear types - like a safe version of an iterator. Certainly I'd be excited to try - I'm not claiming this is immediately production-quality). Or one could ask where the string is coming from in the first place, and trust some kind of fusion-style optimization to remove the intermediate datastructure entirely at runtime.
Peeling off the front 8 or 16 elements should be no harder than peeling off the front 1, though naively you might have to handle each partial case from 1 to 15.
How does that fit
http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html...
That will get you an "unused variable" warning though, which you can suppress by binding to _ instead.
Because there's a tradeoff between ergonomics and static guarantees. A hybrid system (in this case, static tracking of ownership combined with automatic resource destruction) is a valid choice to balance the upsides and downsides of each extreme.
Checks required:
- P2 cannot be changed when P1 is not None. (Run-time check; the compiler has to recognize when it is necessary.)
- P1 can only be set to None or B. (Compile-time check)
- P1 must be set to None before B is destroyed. This avoids a dangling pointer. (Compile-time check when possible, otherwise run-time check.)
- Borrow checking must treat a borrow using P1 as a borrow of B.
These simple rules would maintain the invariant for the backpointer. This allows doubly-linked lists without unsafe code. The backpointer is "weak" and doesn't count as ownership. It's basically weak pointers with a count of either 0 or 1.
It's a slippery slope argument: if you add this, why stop there? Especially if you require run-time checks.
If there was a compelling set of operation that preserved the invariants without run-time checks, and it was expressive, i.e. it covered a large number of cases that you'd otherwise had to put into "unsafe" and it didn't ruin type inference ...
People used to code like that, mostly in assembler and sometimes in C. It's not necessary for functionality. It's just an optimization. One that needs to be justified with benchmarks. Also, it's not at all clear that use of that module is safe.
I'm beginning to think there's a cult of l33t unsafe Rust programming, where people who write unsafe code think they're cool. I used to say that the way to cure new programmers of that is to put them on crash dump analysis for a few months. After they've found pointer bugs in other people's code, they'll have a better sense of why pointer safety is important.
I've worked with people who have the benchmarks to back it up; pointer traversals are expensive.
> people who write unsafe code think they're cool
I've tended to find the opposite: most of the Rust programmers I run into treat unsafe code as an occasionally necessary evil, and every time they write it they think about how the landscape could be improved so they wouldn't have had to, or how to encapsulate it in a separate crate with a small surface area.
oh, and:
The first step towards wisdom is calling things by their right names. —Anonymous Chinese Proverb
The only other fields I know of where things are as badly named are are abstract algebra (ideal, ring, module) and grammar (infinitive, perfect, accusative). It seems to be no coincidence that type theory straddles the two.
Right. I am trying to brighten that line between the sophistication of type systems, the runtime performance of programs and the simplicity of code. I think they are connected in interesting ways, and some of the more rewarding learning I've ever done has consisted of using more sophisticated type system techniques without paying too much on the performance and/or simplicity side of things.
Edit: pages such as https://en.wikipedia.org/wiki/Idempotency_of_entailment, https://en.wikipedia.org/wiki/Monotonicity_of_entailment, https://en.wikipedia.org/wiki/Structural_rule, https://en.wikipedia.org/wiki/Nice_guy, https://en.wikipedia.org/wiki/Linear_logic, https://en.wikipedia.org/wiki/Affine_logic, https://en.wikipedia.org/wiki/Relevance_logic (not sure why "Proper Support" is capitalized, that seems to have no referent)
Hyperlinks allow you to directly look up a term by clicking on it, i.e. are actually useful, whereas trademark symbols are just visual noise. Although of course it is possible to over-link as well, see e.g. the wiktionary FAQ on "wikifying": https://en.wiktionary.org/wiki/Help:FAQ#Wikifying, in practice this doesn't seem to happen; it's more the reverse problem of not putting in enough links.
Then the article makes the "discovery" that "People who say they want Linear™ Types In Rust actually just want Proper Support For Relevant™ Types.", which is pretty obvious if you know this historical context, and coins yet another term, must-use types, which unsurprisingly has no ™ after it.
I think I get what you're trying to do, I myself used ™ for a little bit back 6-7 years ago, a little bit before I wrote http://insearchoftheultimateprogramming.blogspot.com/2011/04.... But ™ just isn't effective; even if you think you know what a term means, you can't explain it except by its relationship to other terms. And once you forget what that ™ symbol referred to you're just as clueless as everyone else. Whereas URLs are "resource locators" and actually clarify what you intended.
I wonder what the upcoming linear types work will do.
I think I under-specified my requirement. :-) By "16 bytes at a time," I mean, "run a single CPU instruction on those 16 bytes."
But yeah, I get your drift. I can see how it might be theoretically possible. I suppose the key gains might be in how much confidence a programmer can have that their code compiles down to the right set of instructions.
In the long term I hope for a "nice" language (in particular one in which checked correctness is easy) with explicit performance semantics along the lines of http://www.cs.cmu.edu/~rwh/papers/iolambda/short.pdf . But yeah under the current state of the art there is no ideal approach, so there's a tradeoff in practice even though I don't think there should be one in theory.
I get that occasionally it's important to know the exact order, and this is where tighter rules and tooling can help. Rust wasn't designed to be an "everything is as explicit as possible" language. (Neither is C, for that matter, ever since compilers stopped paying attention to the "register" keyword…)
In terms of understanding how the code will execute or testing your app, the implicit, confusing rules are less "ergonomic".
(Yes, GCs require tuning and so forth, and that can be a pain, but so does malloc and free, so that's a wash. In most applications you never need to manually tune a GC.)
Destructors are a common resource management idiom there (although I guess most C++ programmers couldn't describe the behavior correctly), and there are no other really common idioms for that.
Better the devil you kind of know?
I wonder if Rust's compile-time meta-programming can be used to implement 'pluggable' linear-types for experiments, maybe along the lines of [1]. That might be a good compromise.
[1] S. Chang, A. Knauth, B. Greenman, Type Systems as Macros. http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf
That is, it's less about order and more about bookkeeping. The ergonomics directly affect code quality.
https://www.reddit.com/r/rust/comments/6a3ac4/the_pain_of_re...
Part of the pain would come from conditionals:
if something {
func(val1);
} else {
func(val2);
}
This is indeed "pain", but of a good kind (at least it if the error message is decent).
I admit there are harder cases:
if(foo)
func(val1)
else
func(val2)
... do something that doesn't change foo or use val1, val2
...
if(!foo)
func(val1)
else
func(val2)
That makes the "trivialness" of a destructor part of the interface, which is a price. But then from my experience in C++, we pay that price anyway, because to have any sort of assurance about what you are doing, you need some clue about what the destructor does.
I guess it makes sense, his most recent papers are about indeterminism (http://www.pitt.edu/~belnap/futurecontingents.pdf), which logic doesn't handle well, but I'm not quite sure how you'd represent the branching-universe model he uses in a type system. I guess you'd need the history operator he uses, m/h = moment m on history h.