In computing, a unique type guarantees that an object is used in a single-threaded way, with at most a single reference to it. If a value has a unique type, a function applied to it can be optimized to update the value in-place in the object code. Such in-place updates improve the efficiency of functional languages while maintaining referential transparency. Unique types can also be used to integrate functional and imperative programming.
Uniqueness typing is best explained using an example. Consider a function
readLine that reads the next line of text from a given file:
function readLine(File f) returns String return line where String line = doImperativeReadLineSystemCall(f) end end
doImperativeReadLineSystemCall reads the next line from the file using an OS-level system call which has the side effect of changing the current position in the file. But this violates referential transparency because calling it multiple times with the same argument will return different results each time as the current position in the file gets moved. This in turn makes
readLine violate referential transparency because it calls
However, using uniqueness typing, we can construct a new version of
readLine that is referentially transparent even though it's built on top of a function that's not referentially transparent:
function readLine2(unique File f) returns (File, String) return (differentF, line) where String line = doImperativeReadLineSystemCall(f) File differentF = newFileFromExistingFile(f) end end
unique declaration specifies that the type of
f is unique; that is to say that
f may never be referred to again by the caller of
readLine2 returns, and this restriction is enforced by the type system. And since
readLine2 does not return
f itself but rather a new, different file object
differentF, this means that it's impossible for
readLine2 to be called with
f as an argument ever again, thus preserving referential transparency while allowing for side effects to occur.
Relationship to linear typing
The term is often used interchangeably with linear type, although often what is being discussed is technically uniqueness typing, as actual linear typing allows a non-linear value to be "cast" to a linear form, while still retaining multiple references to it. Uniqueness guarantees that a value has no other references to it, while linearity guarantees that no more references can be made to a value.
- Haller, P.; Odersky, M. (2010), "Capabilities for uniqueness and borrowing", ECOOP 2010—Object-Oriented Programming, pp. 354–378
- Philip Wadler (March 1991). Is there a use for linear logic?. p. 7.
||This article's use of external links may not follow Wikipedia's policies or guidelines. (February 2013)|
Discussions of uniqueness typing in programming languages
- Lively Linear Lisp -- 'Look Ma, No Garbage!'
- Linear Logic and Permutation Stacks--The Forth Shall Be First
- Minimizing Reference Count Updating with Deferred and Anchored Pointers for Functional Data Structures
- 'Use-Once' Variables and Linear Objects -- Storage Management, Reflection and Multi-Threading