In
computing
Computing is any goal-oriented activity requiring, benefiting from, or creating computing machinery. It includes the study and experimentation of algorithmic processes, and development of both hardware and software. Computing has scientific, ...
, 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 computing, object code or object module is the product of a compiler
In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ...
. Such in-place updates improve the efficiency of
functional language
In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that ...
s while maintaining
referential transparency
In computer science, referential transparency and referential opacity are properties of parts of computer programs. An expression is called ''referentially transparent'' if it can be replaced with its corresponding value (and vice-versa) withou ...
. Unique types can also be used to integrate functional and imperative programming.
Introduction
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
Now
doImperativeReadLineSystemCall
reads the next line from the file using an
OS-level
system call
In computing, a system call (commonly abbreviated to syscall) is the programmatic way in which a computer program requests a service from the operating system on which it is executed. This may include hardware-related services (for example, acc ...
which has the
side effect
In medicine, a side effect is an effect, whether therapeutic or adverse, that is secondary to the one intended; although the term is predominantly employed to describe adverse effects, it can also apply to beneficial, but unintended, consequence ...
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 (unique 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 system
In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progr ...
. 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 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
monad
Monad may refer to:
Philosophy
* Monad (philosophy), a term meaning "unit"
**Monism, the concept of "one essence" in the metaphysical and theological theory
** Monad (Gnosticism), the most primal aspect of God in Gnosticism
* ''Great Monad'', a ...
s.
A compiler extension has been developed for the
Scala programming language
Scala ( ) is a strong statically typed general-purpose programming language that supports both object-oriented programming and functional programming. Designed to be concise, many of Scala's design decisions are aimed to address criticisms of J ...
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
In film, television, and theatre, typecasting is the process by which a particular actor becomes strongly identified with a specific character, one or more particular roles, or characters having the same traits or coming from the same social or ...
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.
Linearity and uniqueness can be seen as particularly distinct when in relation to non-linearity and non-uniqueness modalities, but can then also be unified in a single type system.
See also
*
Linear type
*
Linear logic
References
{{Reflist
External links
Bibliography on Linear LogicUniqueness Typing Simplified
Type theory