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

41–50 of 82 posts

Re: The Pain of Real Linear Types in Rust

#41

Post by pcwalton »

cwzwarich wrote: post #39
pcwalton wrote: post #34

Earlier quoted context omitted.

Nobody's talking about semantic simplicity; we're talking about developer ergonomics.

If you take the view that code is read more times than it is written (which is lightly amusing given the topic of this thread), then shouldn't you optimize for the ergonomics of reading and understanding code that is already written rather than writing it? I don't see how Rust's choice is defensible from that viewpoint. If I quizzed actual Rust users (rather than the language developers that are posting here) about t…

Usually programmers don't care about the exact order that things are freed in. That's the whole reason why GC's have been so successful in programming languages (not to mention things like ARC, which are still deterministic but obscure).

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…)

Re: The Pain of Real Linear Types in Rust

#42

Post by belovedeagle »

panic wrote: post #38
stuhood wrote: post #35

Earlier quoted context omitted.

This is a really interesting thought. In the presence of must-use types, you'd imagine that types with side effecting Drop impls (like files), would want to migrate to eventually being used/consumed by a "close" method. But doing that safely in the presence of panics would require... exception handlers?...

You could use something like Go's 'defer' statement to ensure 'close' is called before the current function returns.

Which already exists in Rust in the form of... wait for it... the Drop trait. It's the same thing.

Re: The Pain of Real Linear Types in Rust

#43

Post by mafribe »

kibwen wrote: post #28
mafribe wrote: post #26

Earlier quoted context omitted.

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.

Wouldn't that be a good path: start with initial experiments based on types-by-macros, and see how well that works. Can't be worse that C++'s template meta-programming.

Re: The Pain of Real Linear Types in Rust

#44

Post by E6300 »

johncolanduoni wrote: post #14
hyperpape wrote: post #4

Earlier quoted context omitted.

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

I'm just miffed that they're complaining about names that are actual words. How would you like if they were all named after their discoverers, and therefore an a priori undistinguished mishmash of proper names? (cf. separation axioms[1]) [1]: https://en.wikipedia.org/wiki/Separation_axiom

That's pretty funny. I'm sure memorizing the differences between the Hausdorff, the completely Hausdorff, the regular Hausdorff, the normal Hausdorff, the completely normal Hausdorff, and the perfectly normal Hausdorff must be fun.

Re: The Pain of Real Linear Types in Rust

#45

Post by Mathnerd314 »

hyperpape wrote: post #40
Mathnerd314 wrote: post #29

Earlier quoted context omitted.

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…

The bit about erasing seems like a bit of stretch. Belnap taught at least one of his proof theory classes using Restall's "An Introduction to Substructural Logics" as a textbook. (Belnap did make it clear that he didn't think linear logic was relevant to his own philosophical concerns, but that's not the same as saying he bears it some kind of ill-will).

Well, if relevance logic is part of linear logic, and it's a true subsumption relationship, then you're saying Belnap doesn't think relevance logic is relevant anymore. So in other words he's pretty much rejected logic altogether.

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.

Re: The Pain of Real Linear Types in Rust

#46

Post by kibwen »

cwzwarich wrote: post #39
pcwalton wrote: post #34

Earlier quoted context omitted.

Nobody's talking about semantic simplicity; we're talking about developer ergonomics.

If you take the view that code is read more times than it is written (which is lightly amusing given the topic of this thread), then shouldn't you optimize for the ergonomics of reading and understanding code that is already written rather than writing it? I don't see how Rust's choice is defensible from that viewpoint. If I quizzed actual Rust users (rather than the language developers that are posting here) about t…

Code only gets read if it gets written in the first place, which it won't if your fresh new language makes it too hard to bootstrap an ecosystem and a community. One of the foundational premises of this year's ergonomics initiative is that Rust code is still too hard to write; a Rust-like language with linear types instead of destructors would be yet harder to write, and would only improve the ability to reason about code in a small minority of cases. I've been writing Rust code since before it was cool to claim you were doing things "before it was cool", and while I appreciate the cases where people have longed for linear types, I have never needed anything more than what destructors provide (which subverts the very premise of your comment, because, for my uses, enforcing linear types would be harder to both read and write). Nobody on the Rust team is pretending that there aren't tradeoffs.

Re: The Pain of Real Linear Types in Rust

#47

Post by Animats »

The 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?

Re: The Pain of Real Linear Types in Rust

#48

Post by Animats »

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…

Destructors seem to be a pain point for functional programming people. They're inherently imperative; they don't return anything because they have no one to return it to.

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.

Re: The Pain of Real Linear Types in Rust

#49

Post by Veedrac »

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

Ah, but you can fake linear types today! There are ergonomic issues, but it works and it's used in practice.

https://www.reddit.com/r/rust/comments/6a3ac4/the_pain_of_re...

Re: The Pain of Real Linear Types in Rust

#50

Post by matt_kantor »

belovedeagle wrote: post #42
panic wrote: post #38

Earlier quoted context omitted.

You could use something like Go's 'defer' statement to ensure 'close' is called before the current function returns.

Which already exists in Rust in the form of... wait for it... the Drop trait. It's the same thing.

The difference is that Go's `defer` is explicitly written out in the relevant scope, while Rust's `Drop` is implicit and defined elsewhere.
Post reply on HN