Linear type system

Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances. Such systems are useful for constraining access to system resources such as files, locks and memory by keeping track of changes of state that occur and preventing invalid states.

Several type systems have emerged by discarding some of the structural rules exchange, weakening, and contraction:

The explanation for affine type systems is best understood if rephrased as "every occurrence of a variable is used at most once".

Linear types corresponds to linear logic and ensures that objects are used exactly once, allowing the system to safely deallocate an object after its use.

The Clean programming language makes use of uniqueness types (a variant of linear types) to help support concurrency, input/output, and in-place update of arrays.

Linear type systems allow references but not aliases. To enforce this, a reference goes out of scope after appearing on the right-hand side of an assignment, thus ensuring that only one reference to any object exists at once. Note that passing a reference as an argument to a function is a form of assignment, as the function parameter will be assigned the value inside the function, and therefore such use of a reference also causes it to go out of scope.

...
Wikipedia