[kibwen]

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

[mafribe]

   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.

[Gankro]

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.

[johncolanduoni]

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

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

[kibwen]

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

[mafribe]

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

[kibwen]

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

[mafribe]

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

[Veedrac]

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

[kibwen]

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.

[johncolanduoni]

Also known as "the Scala problem" (and I say that as someone who writes a lot of Scala).