Editing Uniqueness type

{{Type systems}}
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 [[Compiler optimization|optimized]] to update the value in-place in the [[object code]]. Such in-place updates improve the efficiency of [[functional 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 <code>readLine</code> that reads the next line of text from a given file:

<!-- unclear what programming language this is -->
<syntaxhighlight lang="text">
function readLine(File f) returns String
    return line where
        String line = doImperativeReadLineSystemCall(f)
    end
end
</syntaxhighlight>
Now <code>doImperativeReadLineSystemCall</code> reads the next line from the file using an [[operating system|OS]]-level [[system call]] which has the [[Side effect (computer science)|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 <code>readLine</code> violate referential transparency because it calls <code>doImperativeReadLineSystemCall</code>.

However, using uniqueness typing, we can construct a new version of <code>readLine</code> that is referentially transparent even though it's built on top of a function that's not referentially transparent:
<syntaxhighlight lang="text">
function readLine2(unique File f) returns (unique File, String)
    return (differentF, line) where
        String line = doImperativeReadLineSystemCall(f)
        File differentF = newFileFromExistingFile(f)
    end
end
</syntaxhighlight>
The <code>unique</code> declaration specifies that the type of <code>f</code> is unique; that is to say that <code>f</code> may never be referred to again by the caller of <code>readLine2</code> after <code>readLine2</code> returns, and this restriction is enforced by the [[type system]]. And since <code>readLine2</code> does not return <code>f</code> itself but rather a new, different file object <code>differentF</code>, this means that it's impossible for <code>readLine2</code> to be called with <code>f</code> 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 (programming language)|Clean]], [[Mercury (programming language)|Mercury]], [[SAC_programming_language|SAC]] and [[Idris (programming_language)|Idris]]. They are sometimes used for doing [[I/O]] operations in functional languages in lieu of [[Monads in functional programming|monad]]s.

A compiler extension has been developed for the [[Scala (programming language)|Scala programming language]] which uses annotations to handle uniqueness in the context of message passing between actors.<ref>{{citation|last1=Haller|first1=P.|last2=Odersky|first2=M.|authorlink2=Martin Odersky|year=2010|contribution=Capabilities for uniqueness and borrowing|title=ECOOP 2010—Object-Oriented Programming|pages=354–378|url=http://lampwww.epfl.ch/~phaller/doc/capabilities-uniqueness2.pdf}}</ref>

==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 [[Type casting (computer programming)|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.<ref>{{cite conference |first=Philip |last=Wadler |authorlink=Philip Wadler |title=Is there a use for linear logic? |conference=ACM SIGPLAN symposium on partial evaluation and semantics-based program manipulation (PEPM '91) |date=17–19 June 1991 |url=http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html#linearuse |pages=255–273 |doi=10.1145/115865.115894 |isbn=0-89791-433-3 |citeseerx=10.1.1.26.4202}}</ref>

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. <ref>{{cite conference |first1=Daniel | last1=Marshall |first2=Michael |last2=Vollmer |first3=Dominic| last3= Orchard| title=Linearity and Uniqueness: An Entente Cordiale|conference=ESOP'22 |date=7 April 2022|doi=10.1007/978-3-030-99336-8_13|doi-access=free}}</ref>

==See also==
*[[Linear type]]
*[[Linear logic]]

==References==
{{Reflist}}

==External links==
* [https://www.cs.cmu.edu/~carsten/linearbib/llb.html Bibliography on Linear Logic]
* [http://www.edsko.net/pubs/ifl07-paper.pdf Uniqueness Typing Simplified]

[[Category:Type theory]]