Linear Types

LinearTypes are types whose instances must be held in LinearVariable?s. LinearVariable?s must be accessed exactly once in their scope; linear objects' reference count is always exactly 1. This allows them to avoid synchronisation and garbage collection; for the same reason, in-place update of linear objects is also referentially transparent. Linear objects are ideal for representing non-shareable resources; for example, I/O streams. Since it makes little sense to have multiple readers or writers active simultaneously, the stream can be modeled as a linear object. Other examples include hardware resources in a reflective system, such as the CPU or heap.

The best description of linear types and their advantages is probably HenryBaker's papers on the subject:

Other papers:

"Linear types can change the world!" (1990) and "A taste of linear logic" (1993) by PhilipWadler (available from http://www.research.avayalabs.com/user/wadler/topics/linear-logic.html working link http://web.archive.org/web/20030219075959/http://www.research.avayalabs.com/user/wadler/topics/linear-logic.html) Another working link(from PhilipWadler's homepage): http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html

Also, "Adoption and Focus: Practical Linear Types for Imperative Programming":

http://research.microsoft.com/vault/learn/papers/pldi02.pdf

AdvancedTopicsInTypesAndProgrammingLanguages devotes a chapter to the subject (OK, to linear types and related stuff).

See also OnMonads. A monad and a linear type address the same problem in FunctionalProgramming. (Monoids in CategoryTheory are the source of inspiration.)

Functional programming is based on the mathematical definition of a function, a map from a domain to a range. For each element x in the domain, there is one, only one, and always the same one corresponding element y. Mutable state in a programming language usually ruins the mathematical notion of a function. If a function f is based on mutable state, then x may map to y1 when the program is in state t1 and then may map to y2 when the program is in state t2.

Linear types and monads (OnMonads) are mechanisms to enforce a linear view of mutable state. A function can pass the global state to the functions it depends on. It can also return the global state as part of its result. If it wants to modify that state, it simply substitutes a different global state. The global state is part of the domain and the range, and it may be changed by substitution rather than mutation. This is still the mathematical notion of a function.

For efficiency, a function can mutate the global state it received rather than substitute a different global state if and only if it can prove that no other function will be able to detect that a mutation occurred instead of a substitution. Linear types and monads are mechanisms to perform such a proof by type checking at compile time, and at the same time eliminate the need for each function to always pass and return the global state explicitly.

What about a monad on the category of functions with linear types (rather than a monad on the category of sets)?

I'm a bit confused about LinearVariable?s - above, it is asserted that they hold the only pointer to their referent (a bit like RestrictedPointers? in C9X), and so avoid the need for GarbageCollection. However, HenryBaker also discusses the use of LinearVariable?s in an otherwise normal LISP, in an attempt to make ReferenceCounting more efficient in "Minimizing Reference Count Updating with Deferred and Anchored Pointers for Functional Data Structures" (http://home.pipeline.com/~hbaker1/LRefCounts.html).

In this context, LinearVariable?s can point to shared objects, but can themselves be used exactly once. Are we sure this is not the case in a fully-linear language?

In the semi-linear LISP, there are two handy functions which aren't otherwise needed: dup, which duplicates a variable, so it can be used twice, and kill, which reads a variable but does nothing with the value (linear variables must be read exactly once - not zero times).

Note that the requirement for exactly one read has implications for conditional structures; both arms of an if-else must use exactly the same variables.

-- TomAnderson

A LinearVariable? is a reference that can be used only once. As such, it's never any more useful to the programmer than having an ordinary variable pointing to the same thing. So, you wouldn't normally be any point in having a LinearVariable? pointing to a shared object - except for HenryBakers cunning optimizations involving reference counting. A LinearObject? is something which is guaranteed referred to only by a single LinearVariable?. kill and dup apply to both: killing a LinearVariable? pointing to a shared object does nothing (well, it cancels the deferred refcount increment); killing a LinearVariable? pointing to a LinearObject? free()s up the object. dup() on a LinearVariable? pointing to a shared object probably just creates a second LinearVariable? (with a 2nd deferred refcount increment); dup() on one pointing to a LinearObject? would have to copy the LinearObject? so that there were now two of them in memory. Which is plausible if it was small/identifiable, but not if it were the entire state of the computer....--AlanLawrence?

Linear form is a bit like the inverse of StaticSingleAssignmentForm - in SSA, variables are assigned to exactly once, whereas in linear form, they are read from exactly once.

Linear typing enforces single reading from the variable in a particular scope. The concept should be extended to multiple reads from the variable in the scope. Any idea , Janjua

The variable must be read exactly once, but the value may be used more than once. Declarative/functional/SSA languages, are capable of handling this nicely. Where redefinition shadows the old definition, we get a handy syntax that mimics that of assignment. So you end up with a brand new linear variable ready to be read from exactly once, without having to introduce a new name into your code for each intermediate definition. CleanLanguage in particular, allows for pretty elegant use of linear types like this (it calls them UniquenessTypes or UniqueTypes). The point linear typing in programming languages is to ensure that references don't diverge from a linear usage, so you can safely push them as far as linear typing will allow. They represent the synchronous nature of safe resource manipulation, in a way that can be enforced at compile time.

CategoryLanguageFeature CategoryLanguageTyping

EditText of this page (last edited December 8, 2014) or FindPage with title or text search