Uniqueness type

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.
Introduction.
Uniqueness typing is best explained using an example. Consider a function codice_1 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
Now codice_2 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 codice_1 violate referential transparency because it calls codice_2.
However, using uniqueness typing, we can construct a new version of codice_1 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 (unique File, String)
 return (differentF, line) where
 String line = doImperativeReadLineSystemCall(f)
 File differentF = newFileFromExistingFile(f)
 end
end
The codice_6 declaration specifies that the type of codice_7 is unique; that is to say that codice_7 may never be referred to again by the caller of codice_9 after codice_9 returns, and this restriction is enforced by the type system. And since codice_9 does not return codice_7 itself but rather a new, different file object codice_13, this means that it's impossible for codice_9 to be called with codice_7 as an argument ever again, thus preserving referential transparency while allowing for side effects to occur.
Programming languages.
Uniqueness types are implemented in functional programming languages such as Clean, Mercury, SAC and Idris. They are sometimes used for doing I/O operations in functional languages in lieu of monads.
A compiler extension has been developed for the Scala programming language which uses annotations to handle uniqueness in the context of message passing between actors.
Relationship to linear typing.
A unique type is very similar to a linear type, to the point that the terms are often used interchangeably, but there is in fact a distinction: actual linear typing allows a non-linear value to be typecast 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.