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

71–80 of 82 posts

Re: The Pain of Real Linear Types in Rust

#71

Post by derefr »

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…

The "point of Rust" is to be the simplest zero-runtime-overhead system to use.

Re: The Pain of Real Linear Types in Rust

#72

Post by derefr »

Animats wrote: post #48
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'…

> They're inherently imperative; they don't return anything because they have no one to return it to.

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

Re: The Pain of Real Linear Types in Rust

#73

Post by jcranberry »

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…

I'm not particularly educated in this issue, but if you're going to use a garbage collector, why not just use a language with a GC that abstracts away memory management completely? Like, what would be the advantages over Java?

Re: The Pain of Real Linear Types in Rust

#74

Post by jcranberry »

haskellandchill wrote: post #3

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

What I find asinine is that the writer says substructural type systems (the concept which the names of the types are inherited from) are badly named, yet I'm somewhat dubious that he knows anything about them? I certainly don't, and although the relationship between affine types and affine spaces is not immediately obvious to me, the relationship between linear types and linearity is very clear.

Re: The Pain of Real Linear Types in Rust

#75

Post by _lm_ »

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…

You might find Idris's totality checking very interesting, if you haven't already seen it!

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html...

Re: The Pain of Real Linear Types in Rust

#76

Post by adrianratnapala »

arjie wrote: post #54
cwzwarich wrote: post #39

Earlier quoted context omitted.

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…

Perhaps this is obvious to everyone else, but it isn't to me. Are you advocating explicitly dropping every variable I create? Like `init; use; drop;` explicitly where right now I essentially do `init; use;` and then there's an implicit drop when we exit scope?

I guess it is only for ones with nontrivial destructors.

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.

Re: The Pain of Real Linear Types in Rust

#77

Post by JoshTriplett »

Animats wrote: post #56
JoshTriplett wrote: post #52

Earlier quoted context omitted.

> 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. There are many more patterns where that came from, and you…

rust "intrusive-collections" crate 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…

> It's not necessary for functionality. It's just an optimization. One that needs to be justified with benchmarks.

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.

Re: The Pain of Real Linear Types in Rust

#78

Post by millstone »

arjie wrote: post #54
cwzwarich wrote: post #39

Earlier quoted context omitted.

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…

Perhaps this is obvious to everyone else, but it isn't to me. Are you advocating explicitly dropping every variable I create? Like `init; use; drop;` explicitly where right now I essentially do `init; use;` and then there's an implicit drop when we exit scope?

You would be required to drop values that aren't moved elsewhere. Currently Rust has a one-bit reference count which dynamically tracks which values need to be dropped. Linear types would transform this into a static property that the compiler checks.

Part of the pain would come from conditionals:

    if something { 
        func(val1);
    } else {
        func(val2);
    }
This would be disallowed because the liveness of val1 and val2 can't be statically known after the conditional.

Re: The Pain of Real Linear Types in Rust

#79

Post by adrianratnapala »

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

It doesn't help to use "actual words" when those words have no discernible relationship to their usage. And I don't just mean "common" usage, but the usage by others in related fields. "affine" and "linear" are commonplace concepts in mathematics, but it is in no way clear how they relate to type systems, let alone what properties a type system has when described as such.

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.

Re: The Pain of Real Linear Types in Rust

#80

Post by adrianratnapala »

millstone wrote: post #78
arjie wrote: post #54

Earlier quoted context omitted.

Perhaps this is obvious to everyone else, but it isn't to me. Are you advocating explicitly dropping every variable I create? Like `init; use; drop;` explicitly where right now I essentially do `init; use;` and then there's an implicit drop when we exit scope?

You would be required to drop values that aren't moved elsewhere. Currently Rust has a one-bit reference count which dynamically tracks which values need to be dropped. Linear types would transform this into a static property that the compiler checks. Part of the pain would come from conditionals: if something { func(val1); } else { func(val2); } This would be disallowed because the liveness of val1 and val2 can't be…

If "val1" and "val2" are really things that have to be used exactly once, then the above code is already in error (unless they are provably the same object), and a compiler with linear types will correctly complain about it.

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)
Is correct, if strange, code which I assume is hard for a compiler to understand. But then it is hard for humans too.
Post reply on HN