A feature available in the CleanLanguage (and some other research languages) where a value of such type must be used in a linear way: there can be only one reference to it at any given time.

UniqueType''''''s are useful to model concepts that require destructive update, including:

* I/O
* imperative data-structures
* files, sockets and other system resources

Very similar to LinearTypes (I'm not sure what the difference is, or whether there is any difference).

----

Like monads, a way of dealing with SideEffect''''''s in languages which do not have them.  If the uniqueness invariant is preserved, then the object can be mutated in place rather than copied everywhere--allowing both the advantages of ReferentialTransparency while having mutable state.  (OTOH, one must ask how Referentially''''''Transparent an expression is if I can't hold on to it forever...)

In FunctionalProgrammingLanguage''''''s, a longstanding technique for writing code which resembles mutable-state code is ''threading'' (which has nothing to do with multithreading or other concurrency mechanisms).  If you have an object which you want to "mutate", you adopt the following conventions in mutator functions:

* "Mutator" functions have both an input and an output parameter corresponding to the object to be "mutated".
* The old value of the mutated object is passed in through the input parameter.
* The function creates a new object, a mutated copy of the old object.
* This is then passed to the caller through the output parameter.
* The caller then uses the "new" object exclusively.

This is called "threading" as objects of this sort were "threaded" through a program.  This technique, while useful, is a pain for the programmer.  Plus, when threading is used, the language may not know that mutable updates are possible.  UniqueType''''''s are a way of formalizing this technique; both to allow the compiler optimization and to avoid the need to declare "threaded" arguments everywhere.

''Was this the motivation for implicit parameters?''

----
When a type is unique, it means that values of that type cannot be duplicated. I.e. if ''world'' 's type is unique, that means that you cannot do the following:

  let world1 = print_line world "Please buy Cincom stock"
  let world2 = print_line world "Please sell Cincom stock"

  sleep (3600*24*7)

  if world.stock_raised "Cincom"
  then world = world1
  else world = world2

Conceptually, the computer has only 1 register that is capable of
holding values of type "world". 

-- StephanHouben

----

I don't quite get it, please help. Suppose I have a simple dag (B->A, C->A)...
* Nope, you've gone off track already, you can't do that. Follow the readings on LinearLogic, that'll help explain the general thinking on the topic.

...and I want to mutate A. How is the threading technique / unique type going to help, since I have (inherently?) two copies of A, corresponding to the two dag pointers. Threading one of them will leave the other one hanging with an old version of A, which is clearly unintended and will fail the unique type check. But then, how do I manage to mutate A at all? -- CristiPp
* As above, your premises and assumptions are simply incorrect; YouCantGetThereFromHere. The whole point, in fact, is to prevent you from doing what you are assuming you want to do.

Note that this sharing of side-effects is intrinsically non-purely functional (break referential transparency), since there is no concept of object identity. IMHO, uniqueness types mostly help make imperative constructs (efficiently) referentially transparent. As always, the problem can be solved with more indirection (very much in the spirit of mutable cells in ML, or the way some Lisp compilers implement mutable closures). You could, in the general case, thread a heap, with pointers represented as keys in that heap. For graphs, the usual representation as a pair of arcs and nodes works fine. -- AnonymousDonor