1. I think it's good enough for concurrency. A big selling point of linear types is that, since there can only be a single reference to a linear value at any time, concurrency is trivial. You just send linear values through other threads on a channel, and they're consumed (from the point of view of the sending thread).
2. The set of types is divided into two universes: the Free universe (i.e. unrestricted) types like bool, int, records and unions containing other free types; and the Linear universe, containing linear types. So non-linear types are allowed and are the default for anything that's not a resource with a particular lifecycle (i.e., anything other than memory, file handles, socket handles, that kind of thing).
3. References are possible and they work like borrowing in Rust.
4. No refcounting or GC, it's done at compile time like in Rust.
I haven't heard much from the usefulness of linear types in real world scenarios and would like to learn more from someone with a bit more experience.
- Is it enough to grow to do things like concurrency?
- Are non-linear types allowed?
- Are references possible?
- In which case, does it fall back to a GC? ref counting?