[clean-list] uniqueness attributes of data constructors

[Arjen van Weelden]

On Sun, 21 Aug 2005, Wolfgang Jeltsch wrote:

> Hello,
>
> in the following mail I use the notation ^*, ^x and ^u/^v for uniqueness
> attributes "unique", "non-unique" and "variable".
>
> I declare a type T via this declaration:
>
> 	:: T a = C (T a -> a)
>
> The type of C is (T^u a^v -> a^v) -> T^u a^v.  This can be specialized to the
> following types:
>
> 	1. (T^* a^v -> a^v) -> T^* a^v
>
> 	2. (T^x a^v -> a^v) -> T^x a^v
>
> Further, I have a function f with type T^* a^v -> a^v.

It seams to me that 2. is not a legal type. I would expect an
uniqueness-attribute-equation [u<=v] added to types like T^u a^v ->
a^v (where ^*<=^*, ^*<=^x, and ^x<=^x).

Or in Clean notation: u:(T v:a) [u<=v].
This makes (T a), *(T a), and *(T *a) legal, but (T *a) illegal.

> Now, I apply C to f which results in a value of type T^* a^v according to the
> first of the above specializations.  I duplicate the reference to the funtion
> application C f which results in the function application having type
> T^x a^v.  Now, I use pattern matching to extract f.  The extracted function

This should yield T^x a^x, I don't know why it doesn't. Are you sure you
did not overlook something. I don't understand why you describe types with
multiple uniqueness-attributes without equations between those attributes.

> has type T^x a^v -> a^v according to the second of the above specializations.
>
> But T^* a^v -> a^v is not a subtype of T^x a^v -> a^v.  In fact, it's the
> other way round.  I could apply the extracted function f to a value of
> non-unique type which shouldn't be possible according to f's original type.
>
> Since I cannot imagine that there is a notable flaw in the uniqueness type
> system, I wonder where my mistake is.  Can somebody explain this to me?

I appears that you ignore uniqueness propagation and/or attribute
equations, which are an important part the the uniqueness type system.

> Best regards,
> Wolfgang

regards,
	Arjen