[clean-list] instantiation of attributed type variables

[Wolfgang Jeltsch]

Am Dienstag, 23. August 2005 09:53 schrieben Sie:
> Hello Wolfgang,
>
> Indeed, the same type variables have the same attributes, not only in type
> declarations but also in function types. In this way typing is preserved
> under substitution. If we would allow a unique variable to be coerced to a
> non-unique one the substitution of a unique function type for such a
> variable would no longer be valid.

Hello,

of course, coercing uniqueness attributes is dangerous but this is not what I 
intended.  Say, we have a type a^* -> a^x (^* standing for "unique" and ^x 
standing for "non-unique").  What's the problem with specializing this to the 
type Int^* -> Int^x?  What I want is to not substitute the variable together 
with its attribute but only the variable, not the attribute.  This is also 
far more intuitive, in my opinion, since the syntax a^* or a^x suggests that 
the uniqueness attribute doesn't have to be replaced since normally variables 
are replaced and the attribute is distinct from the variable.  So in the 
above example, a would be replaced by Int, not a^* by Int^* or a^x by Int^x.

> A substitution of a type for variable in only allowed if these types have
> the same top attribute. This requirement is also present in the type system
> of "Uniqueness Typing for Functional Programming with Graph Rewriting
> Semantics", e.g. in the second rule of def 8.3, page 603.

The strange thing is that in this definition the attribute seems to belong to 
the variable (the rule talks about the attribute of the variable alpha) 
whereas in Clean's syntax the attribute seems to be distinct from the 
variable (it is written besides the variable).

> Now back to your original question, which starts with the declaration
>
> :: T a = C ((T a) -> a)
>
> First of all, this type does not lead to any propagation inequalities,
> since the variable a is not on a propagating position. In fact, variables
> only occurring 'below' an arrow type are not propagating.

I would suggest that variables should only lead to propagation if they appear 
as an argument type of a data constructor and that they lead to propagation 
only in the result type of the constructor and only of this one and only 
constructor.

Take, for example, the List type which is declared as follows:

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

Nil is a data constructor with no arguments so there are no arguments whose 
type is a type variable. Therefore, no propagation should happen.  This mean 
that Nil should have type List^u a^v – without any attribute inequalities.  
This is safe because Nil doesn't contain any elements and therefore there are 
no elements for which indirect sharing could occur.

Cons would get the type a^v (List^u a^v) -> List^u a^v | u <= v because the 
first occurence of the type variable a is as the type of an constructor 
argument and therefore propagation should happen.

Now lets have a type declared as follows:

	:: L a = L (List a)

According to my approach, L would have the type List^u a^v -> L^w a^v.  The 
argument type List^u a^v is not uniqueness propagated, and I think that this 
is fine.

On the other hand, it is dangerous that the inequality w <= u is missing 
because therefore indirect sharing of unique lists is possible.  But I cannot 
see how uniqueness attribution as it is done in Clean or defined in the paper 
solves this problem.  Can somebody explain this to me?

In addition, it seems to me that it is essential that types of data 
constructor arguments which are function types are always attributed with x.  
This is a point, I didn't realize until recently.  Take, for example, the 
type T which is declared as follows:

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

Here, no propagation happens.  We can applied C to a function of unique type, 
duplicate the reference to the result and finally extract the function via 
both references.  So we have essentially duplicated the reference to the 
function which shouldn't be allowed.  How do Clean and the paper deal with 
this problem?

> The application you described and Arjen tried in Clean seems to hit on a
> bug in the uniqueness typing system. What I expected, is the following:
>
> The type constructor T appears on a negative position (i.e. the first
> argument of an arrow type) inside its own definition. This means that the
> coercion behavior of a T-type is contra-variant:  u:(T ..) <= v:(T ..) if v
> <= u.

I don't understand this.  As far as I know, contravariance would mean that
T t1 <= T t2 if t2 <= t1 for any types t1 and t2.  So contravariance has 
something to do with modifying the argument type, not modifying T's 
uniqueness attribute.  Since T is an algebraic type, T^u t <= T^v t iff
u <= v (not v <= u).

What I wanted to say in my previous mail is that assigning the same attribute 
to every occurence of T in the type of C is problematic.  We start with a 
function of type T^* a^v -> a^v and apply C to it.  Because the T in the 
result type has the same attribute as the T in the argument type of the data 
constructor, we get a result of type T^* a^v.  Now we duplicate the reference 
to the result and get the type T^x a^v because of type correction.  If we 
extract our function via pattern matching, the extracted function has type 
T^x a^v -> a^v, again because both occurences of T in C's type have the same 
attribute.  The problem is that we now have a type which is a subtype of the 
original type of the function.

Type correction modifies the attribute of the type constructor which 
corresponds to the type constructor in the data constructor's result type.  
But since there is the rule that all occurences of the type constructor have 
to be equally attributed, type correction finally results in a modification 
of the type of the data constructor argument.  The old data constructor 
argument type is used on the application of the data constructor and the new 
one is used when the argument is extracted again via pattern matching.  So we 
have a type conversion from the old type to the new type which is only safe 
if the old type is a subtype of the new one, not the other way round.

The interesting thing is that according to Arjen's experiment, the Clean 
system doesn't attribute the two occurences of T equally.  Instead, it 
attributes them with independent type variables.  Here the problem is 
different.  Upon application of C the type variable of the left occurence of 
T is instantiated with * whereas upon pattern matching it is instantiated 
with x.

As far as I can see, a solution which is safe would be to give all occurences 
of a type variable the same attribute throughout the data constructor's type, 
respect uniqueness propagation in the liberal sense I explained above and 
apart from this set the remaining attribute positions to x.  Alas, this would 
for example result in the tail of a list being always non-unique even if the 
whole list and the element are unique.

> But when you try it in Clean the results are different, even worse, I 
> think they are wrong. I've briefly looked at the implementation of the
> uniqueness type checker, but was not yet able to see what's going on.
> As soon as I've some more time I'll try to fix the problem.

By the way, I think that on page 81 of the draft version of the Clean 2.0 
Language Report, there is an error.  On the bottom of the page there is a 
definition of "propagating position".  There you have the following sentence:

	A propagating position is characterized by the fact that it is not surrounded
	by an arrow type or by a type constructor with non-propagating arguments.

I think that being surrounded by a type constructor with non-propagating 
arguments is not enough for a position to not be a propagating one.  Instead, 
I would think that the argument the position belongs to has to be a 
non-propagating argument of the type constructor.  Is this correct?

> Regards,
>
> Sjaak Smetsers

Best regards,
Wolfgang Jeltsch