[clean-list] uniqueness attributes of data constructors

[Wolfgang Jeltsch]

Am Montag, 22. August 2005 10:24 schrieben Sie:
> 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.

I see no reason why uniqueness propagation should introduce the inequality
u <= v.  For a type like List the presence of such an inequality would be 
right.  List is declared as follows:

	:: List a = Nil | Cons a (List a)

Values of type a (the element type) may be components of a list since they 
appear as arguments of a data constructor (Cons).  However, with the type 
constructor T and its data constructor C, this isn't the case.  C doesn't 
have an argument of type a.  C is applied to a function, so if this 
function's uniqueness attribute is *, the uniqueness attribute of T a has to 
be *.  Yes, the type of C I mentioned was too loose but considering what I've 
just said, C's type should be this:

	w:(u:(T v:a) -> v:a) -> u:(T v:a) [u <= w]

(I hope, I got the Clean syntax right.)  The difference to your proposal is 
that there is no inequality u <= v but an inequality u <= w.  But since 
u <= x for all attributes u, w could be instantiated with x ("non-unique") so 
that my approach for fooling the type system (see below) would still be 
possible.

Apart from this, even if your inequality u <= v is right, my approach of doing 
this dangerous type conversion for f would still work, wouldn't it?  You 
would just have to replace v by x ("non-unique").  The key point of my 
approach is to modify the attribute of T a.  The attribute of the type 
variable a doesn't matter and can be whatever fits.

> > 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.
>
> 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.

The reason was that I thought that there were no constraints on the attribute 
variables in this example.

> > Now, I use pattern matching to extract f.  The extracted function
> > 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?

> [...]

Best regards,
Wolfgang