A linear type system is a particular form of type system

Type system

A type system associates a type with each computed value. By examining the flow of these values, a type system attempts to ensure or prove that no type errors can occur...

 used in a programming language

Programming language

A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....

. Linear type systems allow reference

Reference (computer science)

In computer science, a reference is a value that enables a program to indirectly access a particular data item, such as a variable or a record, in the computer's memory or in some other storage device. The reference is said to refer to the data item, and accessing those data is called...

s but not alias

Aliasing (computing)

In computing, aliasing describes a situation in which a data location in memory can be accessed through different symbolic names in the program. Thus, modifying the data through one name implicitly modifies the values associated to all aliased names, which may not be expected by the programmer...

es. To enforce this, a reference goes out of scope

Scope (programming)

In computer programming, scope is an enclosing context where values and expressions are associated. Various programming languages have various types of scopes. The type of scope determines what kind of entities it can contain and how it affects them—or semantics...

 after appearing on the right-hand side of an assignment

Assignment (computer science)

In computer programming, an assignment statement sets or re-sets the value stored in the storage location denoted by a variable name. In most imperative computer programming languages, assignment statements are one of the basic statements...

, thus ensuring that only one reference to any object exists at once. Note that passing a reference as an argument

Parameter (computer science)

In computer programming, a parameter is a special kind of variable, used in a subroutine to refer to one of the pieces of data provided as input to the subroutine. These pieces of data are called arguments...

 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.

A linear type system is similar to C++

C++

C++ is a statically typed, free-form, multi-paradigm, compiled, general-purpose programming language. It is regarded as an intermediate-level language, as it comprises a combination of both high-level and low-level language features. It was developed by Bjarne Stroustrup starting in 1979 at Bell...

's auto ptr

Auto ptr

auto_ptr is a class template available in the C++ Standard Library that provides some basic RAII features for C++ raw pointers....

 class

Class (computer science)

In object-oriented programming, a class is a construct that is used as a blueprint to create instances of itself – referred to as class instances, class objects, instance objects or simply objects. A class defines constituent members which enable these class instances to have state and behavior...

, 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

Compile time

In computer science, compile time refers to either the operations performed by a compiler , programming language requirements that must be met by source code for it to be successfully compiled , or properties of the program that can be reasoned about at compile time.The operations performed at...

, whereas auto_ptr can only raise exception

Exception handling

Exception handling is a programming language construct or computer hardware mechanism designed to handle the occurrence of exceptions, special conditions that change the normal flow of program execution....

s 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
  ATS (programming language)
  ATS is a programming language whose stated purpose is to support theorem proving in combination with practical programming through the use of advanced type systems. The performance of ATS has been demonstrated to be comparable to that of the C and C++ programming languages...
  
  
• Mercury
• LinearML
• ALMS
• F*