Uniqueness type
Encyclopedia
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
. 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.
function readLine(File f) returns String
return line where
String line = doImperativeReadLineSystemCall(f)
end
end
Now
-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
However, using uniqueness typing, we can construct a new version of
function readLine2(unique File f) returns (File, String)
return (differentF, line) where
String line = doImperativeReadLineSystemCall(f)
File differentF = newFileFromExistingFile(f)
end
end
The
. And since
operations in functional languages in lieu of monad
s.
Computing
Computing is usually defined as the activity of using and improving computer hardware and software. It is the computer-specific part of information technology...
, 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
Compiler optimization
Compiler optimization is the process of tuning the output of a compiler to minimize or maximize some attributes of an executable computer program. The most common requirement is to minimize the time taken to execute a program; a less common one is to minimize the amount of memory occupied...
to update the value in-place in the object code
Object code
Object code, or sometimes object module, is what a computer compiler produces. In a general sense object code is a sequence of statements in a computer language, usually a machine code language....
. 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 functionreadLine 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
doImperativeReadLineSystemCall reads the next line from the file using an OSOperating system
An operating system is a set of programs that manage computer hardware resources and provide common services for application software. The operating system is the most important type of system software in a computer system...
-level system call
System call
In computing, a system call is how a program requests a service from an operating system's kernel. This may include hardware related services , creating and executing new processes, and communicating with integral kernel services...
which has the side effect
Side effect (computer science)
In computer science, a function or expression is said to have a side effect if, in addition to returning a value, it also modifies some state or has an observable interaction with calling functions or the outside world...
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 doImperativeReadLineSystemCall.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
The
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 after readLine2 returns, and this restriction is enforced by the type systemType system
A type system associates a type with each computed value. By examining the flow of these values, a type system attempts to ensure or prove that no type errors can occur...
. 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.Programming languages
Uniqueness types are implemented in the functional programming languages Clean and Mercury. They are sometimes used for doing I/OI/O
I/O may refer to:* Input/output, a system of communication for information processing systems* Input-output model, an economic model of flow prediction between sectors...
operations in functional languages in lieu of monad
Monads in functional programming
In functional programming, a monad is a programming structure that represents computations. Monads are a kind of abstract data type constructor that encapsulate program logic instead of data in the domain model...
s.
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.External links
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