Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Pain of Real Linear Types in Rust

gankro.github.io

Post reply on HN
Print view View original

21–30 of 82 posts

Re: The Pain of Real Linear Types in Rust

#21

Post by cwzwarich »

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

Re: The Pain of Real Linear Types in Rust

#22

Post by kibwen »

mafribe wrote: post #19
kibwen wrote: post #17

Earlier quoted context omitted.

Pragmatic concerns appear to be the bulk of this argument against them.

Such questions are best answered after MLoC or GLoCs have been written.

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

Re: The Pain of Real Linear Types in Rust

#23

Post by johncolanduoni »

I 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

Re: The Pain of Real Linear Types in Rust

#24

Post by johncolanduoni »

kibwen wrote: post #22
mafribe wrote: post #19

Earlier quoted context omitted.

Such questions are best answered after MLoC or GLoCs have been written.

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

Also known as "the Scala problem" (and I say that as someone who writes a lot of Scala).

Re: The Pain of Real Linear Types in Rust

#25

Post by Gankro »

cwzwarich wrote: post #21

A 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 typ…

Yeah dropck is a fun little gem, which has received several post-1.0 revisions due to soundness problems.

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

Re: The Pain of Real Linear Types in Rust

#26

Post by mafribe »

kibwen wrote: post #22
mafribe wrote: post #19

Earlier quoted context omitted.

Such questions are best answered after MLoC or GLoCs have been written.

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

I 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

Re: The Pain of Real Linear Types in Rust

#27

Post by kibwen »

cwzwarich wrote: post #21

A 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 typ…

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

Re: The Pain of Real Linear Types in Rust

#28

Post by kibwen »

mafribe wrote: post #26
kibwen wrote: post #22

Earlier quoted context omitted.

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

I 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

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

Re: The Pain of Real Linear Types in Rust

#29

Post by Mathnerd314 »

Gankro wrote: post #11
Mathnerd314 wrote: post #10

Earlier quoted context omitted.

Yeah, 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/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/Af…

Literally the only link in the article, on the first use of the Official Terminology, is a link to the wikipedia page that defines all the terms.

And that's not really sufficient; words have a life of their own and take on contextual meanings outside of whatever scope they're introduced in. Case in point, linear types come from linear logic, by Girard, whereas relevant types come from unrelated older work by Belnap and Anderson. The simple act of putting them under one umbrella term, "substructural types", erases the older work and means that the article will focus more on Girard's perspective of logic.

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.

Re: The Pain of Real Linear Types in Rust

#30

Post by cwzwarich »

Gankro wrote: post #25
cwzwarich wrote: post #21

A 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 typ…

Yeah dropck is a fun little gem, which has received several post-1.0 revisions due to soundness problems. 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)`.

The simplest system to use is unrestricted references with some form of automatic garbage collection. If you decide that you want a type system that statically tracks resource utilization, why stop halfway at something that only partially solves the problem? I guess you could one-up linear types here and ask for a type system that makes all creation and destruction of information explicit, e.g. https://www.cs.indiana.edu/~sabry/papers/reversible-logic.pd..., but this is probably a more useful route to explore for a hardware design language than a software programming language.
Post reply on HN