Linear types for programmers
L inear 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.
\(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 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\).
