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

31–40 of 82 posts

Re: The Pain of Real Linear Types in Rust

#31

Post by lmm »

burntsushi wrote: post #12
lmm wrote: post #5

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

Friendly 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 describi…

In practice, probably not.

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.

Re: The Pain of Real Linear Types in Rust

#32

Post by cwzwarich »

kibwen wrote: post #27
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…

It'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.

Re: The Pain of Real Linear Types in Rust

#33

Post by pcwalton »

cwzwarich wrote: post #30
Gankro wrote: post #25

Earlier quoted context omitted.

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…

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

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.

Re: The Pain of Real Linear Types in Rust

#34

Post by pcwalton »

cwzwarich wrote: post #32
kibwen wrote: post #27

Earlier quoted context omitted.

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…

It'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.…

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

Re: The Pain of Real Linear Types in Rust

#35

Post by stuhood »

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…

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

Re: The Pain of Real Linear Types in Rust

#36

Post by SomeStupidPoint »

pcwalton wrote: post #34
cwzwarich wrote: post #32

Earlier quoted context omitted.

It'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.…

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

And more specifically developer writing ergonomics.

In terms of understanding how the code will execute or testing your app, the implicit, confusing rules are less "ergonomic".

Re: The Pain of Real Linear Types in Rust

#37

Post by pcwalton »

SomeStupidPoint wrote: post #36
pcwalton wrote: post #34

Earlier quoted context omitted.

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

And more specifically developer writing ergonomics. In terms of understanding how the code will execute or testing your app, the implicit, confusing rules are less "ergonomic".

Is GC less ergonomic than C-style malloc/free? I don't think so, and not only when writing code. It makes things easier all around.

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

Re: The Pain of Real Linear Types in Rust

#38

Post by panic »

stuhood wrote: post #35
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…

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.

Re: The Pain of Real Linear Types in Rust

#39

Post by cwzwarich »

pcwalton wrote: post #34
cwzwarich wrote: post #32

Earlier quoted context omitted.

It'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.…

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 the invisible control-flow created by the compiler, I doubt very many of them would get it right.

Re: The Pain of Real Linear Types in Rust

#40

Post by hyperpape »

Mathnerd314 wrote: post #29
Gankro wrote: post #11

Earlier quoted context omitted.

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…

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).
Post reply on HN