[gavinray]

Disclaimer: I'm not very bright, and don't write Idris

My understanding of "Linear Types" is that they are geared towards declaring values/types that can be used only once.

If this sounds weird, I thought so too. Except it turns out there a number of (fairly common) scenarios in which you might want to ensure that a value is only possible to be used once.

I've drank too much so I can't conjure many to mind, but what I can think of is something like a buffer in a lexer, where you want to ensure that a token is consumed once and then not available.

There are some decent examples in the Tweag repo for the GHC Linear Types proposal:

https://github.com/tweag/linear-base/tree/master/examples

[dwohnitmok]

> I've drank too much so I can't conjure many to mind

The OP has some examples. One of them is creating verified state machines (i.e. stating invariants that different states and transitions should obey all the way up to entirely specifying the abstract state machine). The paper uses linear types to replace Idris 1's ST type. Another is enforcing order of messages to be sent in a bidirectional communication protocol. There's also a lot more low-level examples (make sure that files get closed after use, make sure mutable variables are used correctly, etc.).

In general invariants of the form "verify that this happens after that happens" (and note that this phrase has two meanings which both are covered, verify that e.g. a clean up action always occurs when an action that requires clean up has happened and also verify that e.g. an action occurs after another action, and not before) can be enforced by linear types, which covers a large amount of what happens with stateful computing.

[paavohtl]

As a practical example Rust uses a less powerful version of linear types called affine types for its ownership system. Values are moved by default in assignments and function calls, and they cannot be used (in their original location) after the move.

[iopq]

Rust already has the ability to make you use the type at most once, so the useful extension for Rust would be "must-use types" which is an extension of linear types (since linear types would be able to represented in this system easily enough)

It would actually solve a lot of issues in Rust, but unfortunately would be an insane amount of work to introduce because they would invade a lot of the current type system

[paavohtl]

There is the #[must_use] attribute for function return values, which throws compiler warnings when results are unused. It is not a real part of the type system though, but it serves as a useful lint.