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.
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.
withFile :: FilePath -> IOMode -> (Handle -> IO r) -> IO r
open file A
do stuff
open file B
do stuff
close file A
do stuff
close file B
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.
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)
There’s also quite a design space still to be explored for these ideas. Even / especially for languages like Haskell.
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.
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.
There's many other such modal type systems/logics used for other special purposes like temporal logic.