Talk:Uniqueness type

Latest comment: 6 years ago by Andreasabel in topic Section on Relationship to linear typing

Benefit?

edit

The Introduction section describes Uniqueness, but I'm left wondering what the benefit of the extra complexity is. Regards, Ben Aveling 09:16, 7 September 2008 (UTC)Reply

The uniqueness property makes it possible to do destructive in-place updates since it can be guaranteed that no other references to the data exist. It also makes it illegal to e.g. erroneously read from a file using the same file handle (call-by-need strategy is free to memoize the subsequent calls which makes them side effect free). For instance in Clean you can write the FFI for a C function in such way that the call passes through the unique handle (unmodified) and returns a tuple (ret_value, handle). Miasmator (talk) 06:44, 17 October 2010 (UTC)Reply

introduction example is wrong?

edit

I think that the introduction example is based on a conceptual error. Referential transparency means that f(x) should return the same value as long as x has the same value. In the case of an object, this could be reworded "x is in the same state". In the example:

function readLine(File f) returns String

the parameter is a 'File'. We are thus tempted to consider f the same way we consider files on a disk, or inside a file system: they are stable packs of data as long as not explicitely changed. But a 'File' in a programming language is instead a purely abstract representation of a real file that provides the information and references the programmer needs to operate on the real file via the OS.

Concretely, a File object holds a pointer attribute that tells where we currently are inside the file. (Actually, the OS representaton of a file also holds it, but we forget it when we think at a file on a disk.) So that consecutive calls to readLine above will not pass the same object/value, f will be each time in a different state: and consistently the function will not return the same value.

To make this explicit, just change the function definition to:

function readLine(DiskFile f, Integer pointer) returns String

or to

function readLine(PointedFile f) returns String

Imo, both of these formulations make it clear that readLine actually is referentially transparent.

--Denispir (talk) 09:58, 20 February 2009 (UTC)Reply

No it isn't. You can operate on the same file at the same place but the file contents could have changed since you last read from it. This is a very simple point.—greenrd (talk) 14:00, 20 February 2009 (UTC)Reply
Further, you're referring to the non-referentially transparent version of the function! The transparent version is function readLine2(unique File f) returns (File, String). Note how a new File is returned to account for the change of state. The file abstraction is standard in programming languages. No need to give it a more obtuse name. --Cybercobra (talk) 18:28, 20 February 2009 (UTC)Reply
I think the example is wrong, but not for this reason. First, I don't understand why this imaginary language was chosen here. Neither of the two languages mentioned in the article use this syntax. My guess is that the author wanted to make the code simpler by using an imperative language. Second, the text mentions "a unique type guarantees that an object is used in a single-threaded way, with at most a single reference to it". However, the reference to the file is used twice in the function. For example Clean uses functions that return a tuple of File* and the read data. Third, the reference "Uniqueness Typing Simplified" isn't probably the best source for information, I'd mention the original Clean papers and thesis "Making Uniqueness Typing Less Unique" instead Demise666 (talk)

Section on Relationship to linear typing

edit

I think the current text is incomprehensible. It should be expanded to a more comprehensible form, for instance via an example. The current text is the following:

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 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. — Preceding unsigned comment added by Andreasabel (talkcontribs) 14:45, 19 February 2018 (UTC)Reply