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.

Contents 1 Introduction 2 Programming languages 3 Relationship to Linear typing 4 See also 5 External links 5.1 Discussions of uniqueness typing in programming languages 5.2 Experiments with uniqueness typing (from a performance perspective) 6 References

[edit] Introduction

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'.

[edit] 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.

[edit] 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. ^[1]

[edit] See also

• Linear type
• Linear logic

[edit] External links

• Bibliography on Linear Logic
• Uniqueness Typing Simplified
• Philip Wadler's writings on linear logic

[edit] 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

[edit] Experiments with uniqueness typing (from a performance perspective)

• A "Linear Logic" Quicksort
• The Boyer Benchmark Meets Linear Logic
• Sparse Polynomials and Linear Logic

[edit] References

1. ^ Philip Wadler (March 1991). "Is there a use for linear logic?". 7