Linear type system

Type systems
Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing

A linear type system is a particular form of type system used in a programming language. 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. Linear typing is related to uniqueness typing but is generally more restrictive.

Affine types are a weaker version of linear types; an affine resource can only be used once, while a linear one must be used once.

In general, these type systems form a family of substructural type systems based on substructural logics.

A linear type system is similar to C++'s auto_ptr class, which behaves like a pointer but is invalidated by being set to null after use in an assignment. However, the linearity constraint can be checked at compile time, whereas auto_ptr can only raise exceptions at run-time if it is misused.

Example code

This example uses C++-like notation, but shows a language with a linear type system (which therefore is not C++).

Dog* d = new Dog( name="Fido" ); // creates a reference to a new object.
Dog* p = d;                      // uses d to create a reference denoted by p to the object
                                 // referred to by d.
                                 // this forces d out of scope, thus d cannot be legally
                                 // used after the assignment to p.
print p->getName();              // output "Fido".
print d->getName();              // COMPILE-TIME ERROR: d was forced out of scope
                                 // by its use above and is therefore
                                 // no longer a valid variable.

Programming languages

The following programming languages support linear (or affine) types:

• ATS
• Mercury
• LinearML
• ALMS
• F*

See also

• Effect system
• Linear logic
• Affine logic