Introduction §

Linear types are an application to type theory of the discipline of linear logic, first described by Jean-Yves Girard (Girard, 1987). Since its inception it has led to many fruitful discoveries in computer science. In this article I hope to explain why it is so interesting, as well as relate it to concrete tools and practices available to programmers today.

There are four main operators in linear logic:

(A ⊗ B), read A times B, represents an independent pair of values that may be used in any order, similar to the struct in a language like Rust;

(A ⊕ B), read A plus B, represents either an A or a B, and the consumer must be prepared for either possibility, similar to the enum in a language like Rust;

(A \operatorname{&} B), read A with B, is either an A or a B, and the consumer gets to choose which one;

(A \operatorname{⅋} B), read A par B, is an interdependent pair of values presented in an order chosen by the producer, and the consumer must be prepared to respond to them in any order.

A simple form of linear types (specifically MLL, the fragment of linear logic without the additive/‘choice’ operators ⊕ and &) can be encoded as a programming language in which each value can be used, and must be used, exactly once, and popularized by Henry Baker in a series of articles about applying them to remove garbage collection from Lisp. Henry Baker is a prominent Lisp hacker and one of the original creators of the Lisp Machine, which is sometimes considered to have lost to the C-based UNIX machines due to the long and unpredictable ‘pause’ required for garbage collection on the relatively slow hardware of the time. This is the form usually seen in programming languages. For example, a λ-calculus term of type (A \multimap B) is a function that exactly consumes one (A) and produces one (B) — encoding a proof of the linear logic proposition (A^\bot \operatorname{⅋} B).

Applications §

By employing linear types, the programmer can model systems in which using something changes its type. A common example involves a ‘cost’: if I have a vending machine that will give me either a chocolate bar or a packet of crisps for a dollar, I cannot simply put the dollar in twice and get both. Using the dollar for one item consumes the dollar, and it is no longer available to get the other item.

A more usual example in everyday programming involves objects that have certain protocols (a sequencing of the available operations) that must be obeyed. For example, once a file handle has been closed, it can no longer be written to: from the programmer’s perspective, the file handle no longer exists. More sophisticated changes to state, for example an ‘unopened’ file handle whose metadata can be accessed becoming an ‘opened’ file handle to/from which the programmer can write/read data, can be modelled as ‘destroying’ the old object and returning a new one.

A related application is that of a network protocol. For example, on a stream implementing HTTP, the server might expect the client to:

open a socket 1. send headers 1. write a request body 1. read a response

Any misordering of these operations, for example writing the request body before the headers, constitutes an error on the part of the client programmer.

Figure 1. An HTTP request protocol.

Another very important example is that of memory management. Because arbitrary duplication of values is disallowed, it is inherent in the structure of the code exactly how long a value must stay around, and therefore when it is safe to reuse its memory. This allows linear languages, in general, to be safely executed without recourse to a garbage collector, reference counter, or other means of tracking memory references — an important quality in systems languages, where unexpected garbage collection pauses are often not an option. More generally, linear types can be used to bridge the gap between functional and imperative languages. A functional program with linear types can be realized as an imperative program; since there is no way to observe a value twice, the memory area backing that value can be safely reüsed, in effect mutably updating the value, without the possibility of the program observing the change (breaking referential transparency).

Linear types also turn out to be very useful in concurrent programming, for two reasons:

by requiring (through a sequence of consumptions and productions) values to be used in a certain order, they allow the specification of protocols between concurrent components;

and, even more importantly, the separation/joining of resources in ⊗ and ⅋ allows the programmer to specify when sequencing doesn’t need to be respected, while ensuring freedom from deadlocks.

To see the benefits in concurrency, we can stop thinking of the types as typing values, and instead see them as typing processes. In this view, a function type like (A ⊸ B) is a process that expects an (A) and produces a (B) at the same time (in the sense that the process chooses the order in which to interact with these things), while a tensor type like (A ⊗ B) represents a pair of processes A pair of processes in interface only: the computation may be done by a single process, so long as it can behave as if it were two processes, i.e. not have a dependency on being accessed in any particular order. that will produce an (A) and a (B) in any order the consumer desires.

Linear types in use §

No mainstream programming language implements full linear types, but various languages have different weakenings of them. Related substructural types are not uncommon in various more- or less-mainstream programming systems.

Linear types are (experimentally) available in recent GHC Haskell, where they are used to help reason about the performance characteristics of programs.

The C++ unique_ptr type and more generally move semantics can be seen as a form of MLL in which the consumed values can still be accidentally accessed at runtime.

Affine types §

An affine type system is one in which any value can be deleted, but not all values can be copied. Affine types have been made mainstream by Rust, a language with an inherently affine type system. Rust is also interesting for having an ordered type system, one in which certain values must be used before other values.

Uniqueness types §

Uniqueness types provide a stronger form of MLL, one in which not only are values not allowed to be used more than once, but guarantees are made that only one reference can exist to the value at a time. Rust again encodes this in its unique-reference types (spelt mut, for historical reasons) where they are used to restrict the scope of mutation of state and prevent data races. The Clean programming language uses uniqueness types to control side effects while maintaining a purely functional semantics.

Session types §

Session types are a variant of linear types geared explicitly towards expressing a protocol to be enacted by two or more parties over a shared communication channel, and are distinct from linear types in that they make the precise ordering of messages to be sent explicit in the type. Session types are available for use in C, Rust, and Java, amongst other languages.