[clean-list] uniqueness attributes of data constructors

[Arjen van Weelden]

Hello,

I am sorry. Obviously, I did not fully understand your question, and my
reply did not make any sense.

I tried your example in Clean.

:: T a = C ((T a) -> a)

c :: .((.(T .a) -> .a) -> .(T .a))
c = C

g :: .(.(T .a) -> .a, .(T .a) -> .a)
g = case (cf, cf) of (C f1, C f2) -> (f1, f2)
where
	cf = C f

	f :: (T .a) -> .a
	f t = f t

Which means that, according to Clean 2.1.1,
	C has type (T^v a^u -> a^u) -> T^w a^u,
and that the extracted
	f has type T^v a^u -> a^u,
even if the shared (C f) has type T^x a^u.

I don't know why this is, but it appears that you're right about there
being no type contraints in this example.

regards,
	Arjen

On Mon, 22 Aug 2005, Wolfgang Jeltsch wrote:

> 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
> _______________________________________________
> clean-list mailing list
> clean-list at science.ru.nl
> http://mailman.science.ru.nl/mailman/listinfo/clean-list
>