inside the function, and therefore such use of a reference also causes it to go out of scope. A linear type system is similar to C++'s unique_ptr class, which behaves like a pointer but can only be moved (i.e. not copied) in an assignment. Although the linearity constraint is checked at compile time, dereferencing an invalidated unique_ptr causes undefined behavior at run-time. Similarly, the Rust programming language has partial support to linear types through the use of lint annotations but differently from C++ the moved from variable cannot be used again. The single-reference property makes linear type systems suitable as programming languages for quantum computation, as it reflects the no-cloning theorem of quantum states. From the category theory point of view, no-cloning is a statement that there is no diagonal functor which could duplicate states; similarly, from the combinatory logic point of view, there is no K-combinator which can destroy states. From the lambda calculus point of view, a variable x can appear exactly once in a term. Linear type systems are the internal language of closed symmetric monoidal categories, much in the same way that simply typed lambda calculus is the language of Cartesian closed categories. More precisely, one may construct functors between the category of linear type systems and the category of closed symmetric monoidal categories. Affine type systems Affine types are a version of linear types allowing to discard (i.e. not use) a resource, corresponding to affine logic. An affine resource can be used at most once, while a linear one must be used exactly once. Relevant type system Relevant types correspond to relevant logic which allows exchange and contraction, but not weakening, which translates to every variable being used at least once. Programming languages The following programming languages support linear or affine types: C++ ATS Clean Idris Mercury F* LinearML Alms Haskell with GHC 9.0.1 or above. Granule Rust Nim See also Effect system Linear logic Affine logic Notes References Type theory