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

11–20 of 82 posts

Re: The Pain of Real Linear Types in Rust

#11

Post by Gankro »

Mathnerd314 wrote: post #10
bradleyjg wrote: post #7

Earlier quoted context omitted.

Simply saying it is poorly named doesn't, but this sentence: "Just so you can look this stuff up in The Literature, I'll be providing all these bad names with a Trademark of Disdain™, but otherwise I'd prefer to use Rust-centric terminology." pretty clearly does. The TM thing is obnoxious.

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.

Re: The Pain of Real Linear Types in Rust

#12

Post by burntsushi »

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

Re: The Pain of Real Linear Types in Rust

#13

Post by mafribe »

kibwen wrote: post #2

Because it's not entirely clear from the title and introduction, this essay is actually arguing against extending Rust's type system to include linear types, rather than critiquing the type system as it currently exists (which people often colloquially describe as having "linear types" even if it technically doesn't). EDIT: The intro has been updated to be clearer, so now I just look like an idiot. :)

   arguing against
The argument doesn't come from a position of deep understanding of substructural types. Once you have affine types (as Rust does), linear is not really a major step. Whether it's worthwhile from a pragmatic POV is a different question.

Re: The Pain of Real Linear Types in Rust

#14

Post by johncolanduoni »

hyperpape wrote: post #4
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.

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

Re: The Pain of Real Linear Types in Rust

#15

Post by mafribe »

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…

As a typing system developer I suspect there is a hard trade-off / sweetspot between complexity of the types/fold constructs and guarantees that can be enforced by types.

   How does that fit
Probably doesn't and typing systems for general purpose languages will probably have to fall back on general recursion to handle it. And there's nothing wrong with this. Language simplicity is also a virtue. If your recursion is complicated and correctness so important that testing is insufficient, then I recommend post-programming verification with a program logic.

Re: The Pain of Real Linear Types in Rust

#16

Post by johncolanduoni »

mafribe wrote: post #13
kibwen wrote: post #2

Because it's not entirely clear from the title and introduction, this essay is actually arguing against extending Rust's type system to include linear types, rather than critiquing the type system as it currently exists (which people often colloquially describe as having "linear types" even if it technically doesn't). EDIT: The intro has been updated to be clearer, so now I just look like an idiot. :)

arguing against The argument doesn't come from a position of deep understanding of substructural types. Once you have affine types (as Rust does), linear is not really a major step. Whether it's worthwhile from a pragmatic POV is a different question.

> Whether it's worthwhile from a pragmatic POV is a different question.

Which is exactly what they're purporting to answer...

Re: The Pain of Real Linear Types in Rust

#17

Post by kibwen »

mafribe wrote: post #13
kibwen wrote: post #2

Because it's not entirely clear from the title and introduction, this essay is actually arguing against extending Rust's type system to include linear types, rather than critiquing the type system as it currently exists (which people often colloquially describe as having "linear types" even if it technically doesn't). EDIT: The intro has been updated to be clearer, so now I just look like an idiot. :)

arguing against The argument doesn't come from a position of deep understanding of substructural types. Once you have affine types (as Rust does), linear is not really a major step. Whether it's worthwhile from a pragmatic POV is a different question.

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

Re: The Pain of Real Linear Types in Rust

#18

Post by Gankro »

mafribe wrote: post #13
kibwen wrote: post #2

Because it's not entirely clear from the title and introduction, this essay is actually arguing against extending Rust's type system to include linear types, rather than critiquing the type system as it currently exists (which people often colloquially describe as having "linear types" even if it technically doesn't). EDIT: The intro has been updated to be clearer, so now I just look like an idiot. :)

arguing against The argument doesn't come from a position of deep understanding of substructural types. Once you have affine types (as Rust does), linear is not really a major step. Whether it's worthwhile from a pragmatic POV is a different question.

This is really ignoring how relevant and affine types interact with different features. For example, unwinding makes perfect sense with affine, not so with relevant. Rust has unwinding, and no effect system to track whether something can or can't unwind.

I also make it very clear that the implementation is mostly free. It's just using tools we already have with minor tweaks. Most of my issues are exactly the pragmatic matters: your standard library isn't built to handle it, nothing in the ecosystem is built to handle it, and it everyone has to opt into support for backwards compatibility reasons.

Re: The Pain of Real Linear Types in Rust

#19

Post by mafribe »

kibwen wrote: post #17
mafribe wrote: post #13

Earlier quoted context omitted.

arguing against The argument doesn't come from a position of deep understanding of substructural types. Once you have affine types (as Rust does), linear is not really a major step. Whether it's worthwhile from a pragmatic POV is a different question.

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

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

Re: The Pain of Real Linear Types in Rust

#20

Post by burntsushi »

mafribe wrote: post #15
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…

As a typing system developer I suspect there is a hard trade-off / sweetspot between complexity of the types/fold constructs and guarantees that can be enforced by types. How does that fit Probably doesn't and typing systems for general purpose languages will probably have to fall back on general recursion to handle it. And there's nothing wrong with this. Language simplicity is also a virtue. If your recursion is co…

> And there's nothing wrong with this.

Right. I am trying to brighten that line between the sophistication of type systems, the runtime performance of programs and the simplicity of code. I think they are connected in interesting ways, and some of the more rewarding learning I've ever done has consisted of using more sophisticated type system techniques without paying too much on the performance and/or simplicity side of things.

Post reply on HN