uniqueness and strictness unified?

[Sjaak Smetsers]

Erik Zuurbier  wrote:
>
>Is that so? What I meant to say is that an object's TYPE can have the
>uniqueness property, and a function cannot just have unique arguments,
>but also unique results. What else would the following valid lines of
>Clean mean:
>
>:: *State = {gen::Generation, size::CellSize} // from the LifeGame
>openfiles :: !*World -> (!*Files,!*World) // from StdFile
>
>My idea was to go away from the concept that uniqueness be a property
>of just any object's TYPE as in the lines above, but that an asterisk
>(destruction sign) should only occur on the left side of an function-arrow.

Uniqueness is certainly not a property of types. Since all functions are
typed, it is convenient to add extra information to the types to express other
requirements on function arguments such as uniqueness.

Formally, you're right with your remark that uniqueness is an object property.
But that also counts for your system. Your destructiveness indication
implies that there are no further references to the actual argument. In
fact, this is a property of this argument object. Anyhow, if you want to
formalize your system, it is inevitable that you define the semantics of
your annotations. I cannot see how this can be done without taking objects
(or expressions) into account.
But again, the intention of the uniqueness type system is to express
requirements on the reference structure of function arguments, not to
express properties of objects themselves.

The motivation for having unique objects is the following. If F requires a
unique argument and G delivers a unique result then F (G ..) is
type-correct. Moreover, if (G ..) is evaluated then  F (G ..) remains
type-correct. The latter can only be guaranteed if uniqueness is invariant
during evaluation. Among other things, this has been proven for the
uniqueness type system (by the way, this is far from trivial!).

>Nowhere else. It says something about the FUNCTION, namely that the
>function might destroy the argument. I also think the concept of
>destructiveness is easier to explain than the uniqueness-idea (for instance
>after years I honestly still don't understand why the State type above should
>be marked as unique, just because some FUNCTIONs on it might do in-place
>updates).
>
>A simple example to support my idea that maybe uniqueness should not be viewed
>as a typing issue:
>
>Upd1 :: *a -> *a
>Upd1 a = a
>
>Upd2 :: a -> a
>Upd2 a = a
>
>Start :: (Int,Real)
>Start = Upd1 (Upd2 a)
>where a = (1,1.0)
>
>This gives a type error:
>Type error [Test.icl,11,Start]: "argument 1 of Upd1" * attribute required
>but not
>offered at the indicated position: ^ (Int,Real)
>while we can easily check that there is only one reference to (Upd2 a).

This example is too simple to indicate the problems that might occur. It
seems to me that the bodies of Upd1 and Upd2 are not relevant; the only
thing that counts is that Upd1 wants to update its argument destructively.
I've changed the types a bit to illustrate why your sysem (or at least my
interpretation of it) is incorrect.

Upd1 :: *[a] -> *[a]
...
Upd2 :: [a] -> [a]
...

Following your line of reasoning, the function

Start = Upd1 (Upd2 [1])

is well-typed (or well-formed, if you insist on avoiding the word type).

However, this is not safe: Upd2 might turn its unique argument into a
non-unique one. Then it is not allowed for Upd1 to update the incoming list.

With uniqueness types, this situation is prevented as follows.

If Upd2 doesn't change uniqueness properties, it will be typed as

Upd2 :: u:[a] -> u:[a]

Otherwise, the type is

Upd2 :: [a] -> [a].

The latter type will cause that Start is rejected.
To summarize, uniqueness properties of a result type, say of a function g,
can be used to administer the changes in the reference structure of the
arguments of g, due to the evaluation of g.

Sjaak Smetsers