- 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 made to update the value in-place in theobject code . In-place updates improve the efficiency offunctional language s 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
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 endNow
doImperativeReadLineSystemCall
reads the next line from the file using an OS-levelsystem 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 makesreadLine
violate referential transparency because it callsdoImperativeReadLineSystemCall
.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 endThe "
unique
" declaration specifies that the type off
is unique; that is to say thatf
may never be referred to again by the caller ofreadLine2
afterreadLine2
returns, and this restriction is enforced by thetype system . And sincereadLine2
does not returnf
itself but rather a new, different file objectdifferentF
, this means that it's impossible forreadLine2
to be called withf
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/O operations in functional languages in lieu of monads.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. [cite paper |author=Philip Wadler |title=Is there a use for linear logic? |date=March 1991 |url=http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html#linearuse |pages=7 ]ee also
*
Linear type
*Linear logic External links
* [http://www.cs.cmu.edu/~carsten/linearbib/llb.html Bibliography on Linear Logic]
* [https://www.cs.tcd.ie/~devriese/pub/ifl07-paper.pdf Uniqueness Typing Simplified]
* [http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html Philip Wadler's writings on linear logic]Discussions of uniqueness typing in programming languages
* [http://home.pipeline.com/~hbaker1/LinearLisp.html Lively Linear Lisp -- 'Look Ma, No Garbage!']
* [http://home.pipeline.com/~hbaker1/ForthStack.html Linear Logic and Permutation Stacks--The Forth Shall Be First]
* [http://home.pipeline.com/~hbaker1/LRefCounts.html Minimizing Reference Count Updating with Deferred and Anchored Pointers for Functional Data Structures]
* [http://home.pipeline.com/~hbaker1/Use1Var.html 'Use-Once' Variables and Linear Objects -- Storage Management, Reflection and Multi-Threading]Experiments with uniqueness typing (from a performance perspective)
* [http://home.pipeline.com/~hbaker1/LQsort.html A "Linear Logic" Quicksort]
* [http://home.pipeline.com/~hbaker1/LBoyer.html The Boyer Benchmark Meets Linear Logic]
* [http://home.pipeline.com/~hbaker1/LFrpoly.html Sparse Polynomials and Linear Logic]References
Wikimedia Foundation. 2010.