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

61–70 of 82 posts

Re: The Pain of Real Linear Types in Rust

#61

Post by barrkel »

pcwalton wrote: post #41
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…

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

GC lets you write functions that return heap allocated values without worrying about who's responsible for freeing the result. That in turn leads to functional code over procedural, which in turn leads to simpler and easier understood code.

That is, it's less about order and more about bookkeeping. The ergonomics directly affect code quality.

Re: The Pain of Real Linear Types in Rust

#62

Post by hyperpape »

Mathnerd314 wrote: post #45
hyperpape wrote: post #40

Earlier quoted context omitted.

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…

I was referring to the subsumption under substructural logic, not a subsumption under linear logic. Belnap seemed to view linear logic as rather different from his own interests in relevance logic.

Re: The Pain of Real Linear Types in Rust

#63

Post by wtetzner »

etatoby wrote: post #53
johncolanduoni wrote: post #14

Earlier quoted context omitted.

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

There are only two hard things in Computer Science: cache invalidation and naming things. —Phil Karlton oh, and: The first step towards wisdom is calling things by their right names. —Anonymous Chinese Proverb

There are only two hard things in Computer Science: cache invalidation, naming things, and off-by-1 errors.

Re: The Pain of Real Linear Types in Rust

#64

Post by Animats »

mafribe wrote: post #57
Animats wrote: post #48

Earlier quoted context omitted.

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

Destructors seem to be a pain point The problem is not so much typing as such (things that don't return anything but terminate -- as destructors do -- can be typed as Unit) but rather to find a good trade-off between expressivity of the language and simplicity of the typing system. Basically explicit destructors mean the typing system needs to track lifetimes and ownership in some form or shape. There seem to be two…

Think of backpointers as a combination of Rust optional pointers and weak pointers, mostly checked at compile time. The basic rule for backpointers is this: If an type instance A contains a backpointer P1, it must either be a None, or a reference to a type instance B which has exactly one reference P2 to A.

Checks required:

- P2 cannot be changed when P1 is not None. (Run-time check; the compiler has to recognize when it is necessary.)

- P1 can only be set to None or B. (Compile-time check)

- P1 must be set to None before B is destroyed. This avoids a dangling pointer. (Compile-time check when possible, otherwise run-time check.)

- Borrow checking must treat a borrow using P1 as a borrow of B.

These simple rules would maintain the invariant for the backpointer. This allows doubly-linked lists without unsafe code. The backpointer is "weak" and doesn't count as ownership. It's basically weak pointers with a count of either 0 or 1.

Re: The Pain of Real Linear Types in Rust

#65

Post by tatterdemalion »

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…

Its hard for me to imagine that requiring every value to be explicitly dropped would produce code which is easier to read and understand.

Re: The Pain of Real Linear Types in Rust

#66

Post by mafribe »

Animats wrote: post #64
mafribe wrote: post #57

Earlier quoted context omitted.

Destructors seem to be a pain point The problem is not so much typing as such (things that don't return anything but terminate -- as destructors do -- can be typed as Unit) but rather to find a good trade-off between expressivity of the language and simplicity of the typing system. Basically explicit destructors mean the typing system needs to track lifetimes and ownership in some form or shape. There seem to be two…

Think of backpointers as a combination of Rust optional pointers and weak pointers, mostly checked at compile time. The basic rule for backpointers is this: If an type instance A contains a backpointer P1, it must either be a None, or a reference to a type instance B which has exactly one reference P2 to A. Checks required: - P2 cannot be changed when P1 is not None. (Run-time check; the compiler has to recognize whe…

I'm not saying this can't be done, au contraire! Indeed cost coherent programming idioms can be converted into typed language primitives. But there is a price to pay in terms of typing system complexity.

It's a slippery slope argument: if you add this, why stop there? Especially if you require run-time checks.

If there was a compelling set of operation that preserved the invariants without run-time checks, and it was expressive, i.e. it covered a large number of cases that you'd otherwise had to put into "unsafe" and it didn't ruin type inference ...

Re: The Pain of Real Linear Types in Rust

#67

Post by Animats »

moosingin3space wrote: post #60
Animats wrote: post #47

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?

Rust's Result type is a "must use" type, which makes it impossible to skip an error check.

Can you assign it to a variable and then ignore it?

Re: The Pain of Real Linear Types in Rust

#68

Post by mcguire »

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

Keep in mind today Rust is intended to be a better C++. (For loose values of 'intended'.)

Destructors are a common resource management idiom there (although I guess most C++ programmers couldn't describe the behavior correctly), and there are no other really common idioms for that.

Better the devil you kind of know?

Re: The Pain of Real Linear Types in Rust

#69

Post by steveklabnik »

Animats wrote: post #67
moosingin3space wrote: post #60

Earlier quoted context omitted.

Rust's Result type is a "must use" type, which makes it impossible to skip an error check.

Can you assign it to a variable and then ignore it?

Yes, assignment counts as a use.

That will get you an "unused variable" warning though, which you can suppress by binding to _ instead.

Re: The Pain of Real Linear Types in Rust

#70

Post by burntsushi »

lmm wrote: post #31
burntsushi wrote: post #12

Earlier quoted context omitted.

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

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

I think I under-specified my requirement. :-) By "16 bytes at a time," I mean, "run a single CPU instruction on those 16 bytes."

But yeah, I get your drift. I can see how it might be theoretically possible. I suppose the key gains might be in how much confidence a programmer can have that their code compiles down to the right set of instructions.

Post reply on HN