Wadler has a great paper on the subject of applying linearity to tame side effecting systems. There he exploits the inherent sequencing of a strict linear let
let! plus the uniqueness afforded by linearity to ensure that e.g. variables corresponding to resources like files have a unique reference active at any one time and to induce an ordering of effects in an expression that guarantees a reasonable prima fascie semantics. For example:
let y = f(x) in z
Need not necessarily fully evaluate either
f(x) in a functional program unless
z demands the value of
y (say, by case’ing on it). However,
let! y = f(x) in z
requires the evaluation of f(x) be fully sequenced before
z is evaluated. It then becomes trivial to notice that a program like
let! file = readFile(“~/password.txt) in sendFileToHacker(file)
- Have a unique handle to the file in question
- Have that handle be consumed by one use
With pervasive linearity, one can do all kinds of neat things like completely ignore the problem of garbage collection.
Linear type systems are deeply intertwined with concurrency and concurrent semantics. The type of linear pairs, for example, can be interpreted as the type of a parallel computation of each component. Since each component’s computation cannot share data by construction, it is safe for an abstract machine to interpret constructing such a pair as a fork and destructing such a pair as a join. The dual of this being the type of a computation that races threads computing each component. (Think of this as the difference between you being able to select the result you want versus the program picking a result for you). But more to the point, linearity encodes the kinds of constraints that make it possible to safely access data in a destructive manner. That is, write access is strictly limited in a linear system to one logical thread of execution because all sharing of the resource backing linear variables is structurally forbidden. To remove the restriction on variable reads being linear, many more practical (but not strictly linear) systems enable “borrowing” immutable references to variables to gain the ability to share data back, or enable unrestricted copies of linear variables to port them back into non-linear land.
In Swift, we want to shoot for a less restrictive system, since even mixed linearity turns out to be quite difficult to work with in practice. An “Affine” type system is more our style - what would manifest is commonly referred to as moveonly types. The manifesto lays out some syntax and some ideas for what we can build here - deinit in structs is an attractive selling point.