7 ms·
The Pain of Real Linear Types in Rust
- kibwen 9y agoBecause it's not entirely clear from the title and introduction, this essay is actually arguing against extending Rust's type system to include linear types, rather than critiquing the type system as it currently exists (which people often colloquially describe as having "linear types" even if it technically doesn't). EDIT: The intro has been updated to be clearer, so now I just look like an idiot. :)
- mafribe 9y agoarguing against The argument doesn't come from a position of deep understanding of substructural types. Once you have affine types (as Rust does), linear is not really a major step. Whether it's worthwhile from a pragmatic POV is a different question.
- Gankro 9y agoThis is really ignoring how relevant and affine types interact with different features. For example, unwinding makes perfect sense with affine, not so with relevant. Rust has unwinding, and no effect system to track whether something can or can't unwind. 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.
- johncolanduoni 9y ago> Whether it's worthwhile from a pragmatic POV is a different question. Which is exactly what they're purporting to answer...
- kibwen 9y agoPragmatic concerns appear to be the bulk of this argument against them.
- mafribe 9y agoSuch questions are best answered after MLoC or GLoCs have been written.
- kibwen 9y agoThat may be true if your goal is to advance programming language research, but if your goal is to extend a language being used in industry then you don't have the luxury of spending that sort of design and implementation effort if you suspect that the extension will be a boondoggle (especially since backwards-compatibility promises mean that you'll be forced to support those features for the rest of time).
- johncolanduoni 9y agoAlso known as "the Scala problem" (and I say that as someone who writes a lot of Scala).
- mafribe 9y agoI agree. 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 http://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf
- kibwen 9y agoI can offer no proof but I'm Pretty Sure that one could hack together linear types using procedural macros, though I can't posit how nice they would be to use nor how well they would interact with the rest of the language and ecosystem.
- haskellandchill 9y ago> It's poorly named, and so are most of the concepts it introduces 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.
- hyperpape 9y agoRight or wrong, simply saying something is poorly named doesn't show that someone is hostile towards academia. By that standard, most of the academics I know would be hostile to academia, since they invariably think something in their field has a bad name.
- bradleyjg 9y agoSimply saying it is poorly named doesn't, but this sentence: "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.
- tpush 9y agoI think it's it hilarious (and true that academia often chooses poor names).
- Mathnerd314 9y agoYeah, it would be better with coloring. Or better yet hyperlinking to the relevant Wikipedia pages / papers / memes. Edit: pages such as https://en.wikipedia.org/wiki/Idempotency_of_entailment https://en.wikipedia.org/wiki/Idempotency_of_entailment, https://en.wikipedia.org/wiki/Monotonicity_of_entailment https://en.wikipedia.org/wiki/Monotonicity_of_entailment, https://en.wikipedia.org/wiki/Structural_rule https://en.wikipedia.org/wiki/Structural_rule, https://en.wikipedia.org/wiki/Nice_guy https://en.wikipedia.org/wiki/Nice_guy, https://en.wikipedia.org/wiki/Linear_logic https://en.wikipedia.org/wiki/Linear_logic, https://en.wikipedia.org/wiki/Affine_logic https://en.wikipedia.org/wiki/Affine_logic, https://en.wikipedia.org/wiki/Relevance_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 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.
- lmm 9y agoAs a Scala user: the further I've got into a functional/MLey style the more linear my code has become. Options or collections are very naturally handled with "fold" (cata). Loops probably shouldn't be infinite - if you're looping it's usually because you're folding along a data structure, and those ought to be finite (one of the ideas I'm toying with is a type-level natural indexed recursion-schemes like library, to make it easy to construct recursive structures that are known-finite). I don't know if it's where Rust wants to be, but I want a practical-oriented ML-family language that does this.
- burntsushi 9y agoFriendly challenge (because I agree with you, but constantly run into limitations): 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?
- mafribe 9y agoAs a typing system developer I suspect there is a hard trade-off / sweetspot between complexity of the types/fold constructs and guarantees that can be enforced by types. How does that fit Probably doesn't and typing systems for general purpose languages will probably have to fall back on general recursion to handle it. And there's nothing wrong with this. Language simplicity is also a virtue. If your recursion is complicated and correctness so important that testing is insufficient, then I recommend post-programming verification with a program logic.
- burntsushi 9y ago> And there's nothing wrong with this. 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.
- adamnemecek 9y agoCMU has a class on Substructural Logics https://www.cs.cmu.edu/~fp/courses/15816-f16/ https://www.cs.cmu.edu/~fp/courses/15816-f16/ Up until 2012 it was just about Linear Logic IIRC.
- cwzwarich 9y agoA lot of the awkwardness that the author describes comes from destructors, which Rust has taken from C++. In fact, Rust has even inherited the incoherence between destructors and exceptions from C++, due to the lack of a solution to the double-throw problem and the need to write unsafe code that is correct in the face of unwinding. 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-unspecified-drop-order/ 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.
- kibwen 9y agoI agree that dropck is scary and needs more verification before we can have reasonable assurance of its soundness. But you're being unnecessarily reductive here: the tradeoff between control and ergonomics offered by destructors is well-known. If you think Rust is verbose today, imagine a Rust where every value had to be explicitly disposed of in every scope (including temporaries). Graydon was well aware of strictly-linear type systems, and chose to go with destructors for (heh) sound reasons.
- cwzwarich 9y agoIt's not like destructors actually remove the complexity. The extra function call you need to add to replace the destructor is already present in your program; it's merely hidden from view. If you are trying to verify the code you have written (either informally or formally) and want to consider all paths through the program, then you need to include the invisible control-flow created by the compiler for destructors. I don't see how it gets any simpler by not being written in your program.
- johncolanduoni 9y agoI was actually thinking about this precise issue this morning (due to this GitHub issue[1]). I think a valuable middleground would be to include this kind of check even without the ?Leave stuff. In essence, the compiler could just give an error if it would have needed to issue a Drop call anywhere for the type. 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). [1]: https://github.com/gfx-rs/gfx/issues/1216 https://github.com/gfx-rs/gfx/issues/1216
- Animats 9y agoThe author tries too hard to avoid using the word "object". "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?
- moosingin3space 9y agoRust's Result type is a "must use" type, which makes it impossible to skip an error check.
- Animats 9y agoCan you assign it to a variable and then ignore it?
- steveklabnik 9y agoYes, assignment counts as a use. That will get you an "unused variable" warning though, which you can suppress by binding to _ instead.
- Thiez 9y agoHardly impossible, just prefix the expression with `[` and suffix with `]` and the warning is gone. Or with `(` and `,)` (creating a tuple of arity one).