Linear types for programmers

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 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:

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:

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.