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

[mafribe]

Wouldn't that be a good path: start with initial experiments based on types-by-macros, and see how well that works. Can't be worse that C++'s template meta-programming.

[johncolanduoni]

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