Can someone please explain what you can do with linear types? I understand what they are (types which the compiler guarantees are used exactly once), but I don't understand why they're important.
The two most commonly referenced uses are safe mutation and better resource management.
Safe mutation because when I have the only reference to a thing, the rest of the system shouldn't care whether I change it in place or make a new one.
Better resource management because you can be sure opened files are closed exactly once and that nothing tries to use a file after close, even where a bracket pattern doesn't fit (or fits much more loosely).
In both cases, you're not doing anything you couldn't do before, but it lets you do it safely. People speak of performance because (especially in Haskell) mutating without being confident nothing else can see is sufficiently full of footguns that the community happily (... and rightly, IMO) pays small performance penalties for security against them. This lets us remove those performance penalties in more cases.
There's some room for the compiler to notice that something is only referenced in one place and safely convert some things to mutation; again this doesn't strictly need linear types, but linear types may let us do that reasoning locally instead of it requiring whole program analysis.
I’ll also add that you can achieve some of these effects without linear types, but linear types are more flexible. For example, a classic way to work with a file in Haskell is to use the function withFile:
Yeah, this is what I meant by "the bracket pattern" and a canonical case where it "doesn't fit" - I appreciate your spelling it out for those who are less familiar :)
Negative consequences are whatever use-after-close errors you make trying to use the thing you returned. ... but I certainly agree that it's not an error that's made very often, and the flexibility is the bigger point.
The following blog post is referenced in the proposal: https://www.tweag.io/blog/2017-08-03-linear-typestates/ . This is maybe a different aspect than what others have been trying to explain, but I found the socket-based example enlightening.
Type states allow the state of the socket (unbound, bound, listening, closed) to be expressed as a part of the type (a type annotation, if you will) so the compiler can verify that you're not reusing a closed socket, or try to send data over an unbound socket.
Linear types then, allow to express in code how a type (annotation) changes over time (e.g., "bind() takes an unbound socket and returns it an a bound state") so the compiler can statically check that it's in a valid state for every operation.
The way I usually think about it is that it's like the Rust borrowing system but more powerful. If the compiler can be sure a type will be used exactly once, you could for example do automatic memory management by freeing the value directly after it is used. You can also fix a range of multithreading bugs with it, as other people have mentioned.
Finally, it allows you to express more invariants about your data through the type system, hopefully reducing bug counts. As an example, soneone could "implement" a sorting function as `sort xs = []`. This has the correct type signature, but is not a correct implementation of sorting. With linear types you could express that the output has to access the values of the input. (Of course what we'd actually want is to express other invariants for sorting as well, but full dependent types are still some ways off)
Haskell as a language is effectively an experiment to see how much unsafe stuff can be done in a compartmentalized and "safe" manner (see SPJ's "Haskell is useless"), so Linear Types are another road to go down to achieve that goal.
A specific safety article was written up by tweag.io, who wrote a pretty slick set of java bindings. Managing resources between two garbage collectors (ghc and jvm) is error-prone, so they used linear types to help prevent a bunch of the things a person can easily mess up. Their article is pretty good: https://www.tweag.io/blog/2020-02-06-safe-inline-java/
Now one can have mutation by simply returning the mutated value which internally can be implemented as mutation since the type system guarantees that the original value never be used after.
Conceptually, it's purely functional programming where a function consumes a value and returns a new one, under the hood it's understood to be mutation which is possible due to these constraints.
All the use cases I've seen are about optimization.
You can avoid a lot of copying and memory management if you know the value will be used a single time, and then generate another value, that will be used a single time again. It has a very large potential impact, mostly on IO.
To add to other user's comments, linear types are useful for reasoning exactly about (some) imperative constructs, which is really, really hard to do with standard type systems. That's why reliably guaranteeing e.g. why it's still difficult to ensure safe and timely disposal of database connections in Haskell (maybe not now) or Scala, despite their powerful type systems.
There's many other such modal type systems/logics used for other special purposes like temporal logic.
