Uniqueness type
From Wikipedia, the free 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 it can be modified in place improving the efficiency of functional languages while maintaining referential transparency. Unique types can also be used to integrate functional and imperative programming languages.
Essentially, given a function:
f(T* x) -> (T x', S y)
where T and S are types and '*' declares to a variable to be unique, then invoking f like so:
f(a) => b, c
f(a) can never occur again, since by declaring 'x' (and thus 'a') to be unique, it is guaranteed that the value 'a' cannot be used again by the caller following the call to f. And since 'a' goes into f but isn't returned, the value of 'a' cannot come up in the program ever again, precluding any future calls of f(a), thus maintaining referential transparency while allowing destructive changes to be safely made to 'a'.
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.
[edit] See also
- Linear type
- Linear logic
