What are linear types?

Just reading the thread mentioned below, then BAM an unfamiliar term.


Continuing the discussion from SE-0298: Async/Await: Sequences:


I did a quick look up. Linear types lets a type system define entities that can be used exactly once. From the Wikipedia page, there are weakenings for at-least-once, at-most-once, and a strengthening for exactly-once-and-in-order (plus unregulated). I was also intrigued in that this system could help in forming an effect system, whose need in Swift has been brought up sometimes to generalize try/throws and await/async.

How would linear types (or the whole substructural type system) be expressed? Would it be an annotation on functions, function parameters, types, variables, or any and all of those?

1 Like

IIUC:
A type that is "at-most-once" is a type with a private or nonexistent copy operation.
A type that is "at-least-once" is a type with a private or nonexistent deinit.

Expressing these in Swift would probably require the Ownership Manifesto's moveonly contexts,
because all current code assumes copy and deinit to be public.

3 Likes

Hey Daryle, sorry about that.

Linear types are relevant here because they can only be transferred around through "moves", they cannot be duplicated. In the case of the proposal, that would mean that the iterator has a lifetime that is guaranteed to be bound by the loop and is guaranteed to be destroyed on exit in all cases.

Right now, structs are implicitly copyable, and class refrences can "escape". This isn't a common problem, but the ownership model will allows us to define provably correct things that can eliminate some possible bugs in cases like this.

-Chris

5 Likes

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 or x or 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)

Will always

  1. Have a unique handle to the file in question
  2. 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.

4 Likes

It seems the link to that second paper is dead, but luckily it was archived.

I've found uniqueness types to be more friendly and flexible than affine or linear types, personally.

Terms of Service

Privacy Policy

Cookie Policy