Uniqueness type

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 the object code. In-place updates improve the efficiency of functional languages 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 end

Now doImperativeReadLineSystemCall reads the next line from the file using an OS-level system 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 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 (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. 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 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.

Игры ⚽ Нужно решить контрольную?

Look at other dictionaries:

  • Type system — Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing …   Wikipedia

  • Dependent type — Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing …   Wikipedia

  • Nominative type system — Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing …   Wikipedia

  • Document Type Definition — (DTD) is a set of markup declarations that define a document type for SGML family markup languages (SGML, XML, HTML). DTDs were a precursor to XML schema and have a similar function, although different capabilities. DTDs use a terse formal syntax …   Wikipedia

  • Peugeot Type 105 — Infobox Automobile generation name = Peugeot Type 105 manufacturer = S. A. des Automobiles Peugeot parent company = aka = production = 1908 1909 23 produced assembly = predecessor = Peugeot Type 95 successor = class = body style = Full size… …   Wikipedia

  • Linear type system — A linear type system is a particular form of type system used in a programming language. Linear type systems allow references but not aliases. To enforce this, a reference goes out of scope after appearing on the right hand side of an assignment …   Wikipedia

  • Classification of finite simple groups — Group theory Group theory …   Wikipedia

  • Clean (programming language) — Clean Paradigm(s) functional Appeared in 1987 Designed by Software Technology Research Group of Radboud University Nijmegen Stable release …   Wikipedia

  • Linear logic — In mathematical logic, linear logic is a type of substructural logic that denies the structural rules of weakening and contraction . The interpretation is of hypotheses as resources : every hypothesis must be consumed exactly once in a proof.… …   Wikipedia

  • Duck typing — Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”