In Linear Haskell a function may and must use its input exactly once. In regular Haskell this multiplicity is any.
Linear typing is not new. The Idris programming language recently reached version 2. The main advancement in it is its "quantitative" typing, which allows to declare and track such multiplicities. One of the allowed multiplicity is 1, that corresponds to linear typing. Thus Idris has already implemented something more general than what Linear Haskell is. But Idris is not yet ready for industrial adoption. Haskell is. Haskell is a mature, industry-strong language. Among these : the best high level one. Hence this new feature may be important.
What practical use Linear Haskell gives us? In-place rewriting for fast algorithms. Safer usage protocols, for example : checking that a file is opened before use and closed after use and not used after close. All these are possible already in regular Haskell, but linear typing makes it simpler, easier, safer.
Of course regular Haskell as we know and use it now is not replaced, Linear Haskell is only an additional capability. And there is some work being done on multiplicity polymorphism, which would allow us to write functions that can be both regular and linear.
Haskell's linearity is different from "uniqueness" typing. An object of a unique type is guaranteed to have only 1 reference to it. Thus a function recieving a unique input can memory-safely interect with it freely. This is an intuitive idea that was followed by many programming languages, including Rust. But in Linear Haskell the linearity is a property of not things, but their usages - of the functions. In Linear Haskell those are the functions that are either linear or not. Functions do not get any guarantee, but they are the ones that offer guarantee - that they use their input exactly once. In Haskell the other kind of linearity can be restored via continuations.
Haskell's linearity corresponds to linear logic. By this design Haskell yet again shows its attraction towards math. This attraction towards math is in my opinion one important cause that made Haskell the incredible success that it is, and my guess is that this linearity design will be yet an other such good decision. The Idris language also made the change from uniqueness typing to linear functions from version 1 to version 2. [This does not necessarily imply that Rust's design is bad for itself, as Rust, being a low level language, is very different.]
I guess linear typing, but rather the more general quantitative typing will be a stepping stone for dependent typing, which Haskell is heading towards. Richard Eisenberg, who is kinda the main driver of dependent typing in Haskell, already said that they are looking to learn from how Idris 2 fused these 2 capabilities.
Of course this initial implementation of Linear Haskell is poor yet, both in reliability and completeness.
If you want to dive deeper in the topic : here are some links :
- Simon Peyton Jones - Linear Haskell: practical linearity in a higher-order polymorphic language
- The "paper
