[clean-list] instantiation of attributed type variables

[Wolfgang Jeltsch]

Am Montag, 22. August 2005 16:31 schrieb Wolfgang Jeltsch:
> Hello again,
>
> how are type variables instantiated in the uniqueness typing system
> described in "Uniqueness Typing for Functional Programming with Graph
> Rewriting Semantics"?  Is a type variable replaced by a type without a
> top-level attribute (since the variable provides the attribute) or is the
> variable together with the attribute replaced by a uniqueness type which
> has the same attribute.
>
> Take, for example, the type a^* -> a^x where ^* means "unique" and ^x means
> "non-unique".  If the first of the above variants is true, this type can be
> specialized to Integer^* -> Integer^x by replacing a with Integer.  If the
> second variant is true, no specialization is possible, since each occurence
> of the type variable a together with an uniqueness attribute has to be
> replaced with the same attributed type but this type has to have ^* as well
> as ^x as its uniqueness attribute because the type variable a appears with
> both attributes in the above function type.
>
> Best regards,
> Wolfgang

Hello again,

I just discovered that Clean forces the same type variable to have the same 
attribute at every occurence not only in data constructor types but in every 
function type.  Is this restriction also present in the uniqueness type 
system described in the above-mentioned paper?  Isn't this an unnecessary 
restriction?  Isn't this unintuitive since the syntax for types allows you to 
give an uniqueness attribute for every *occurence* of a type variable, 
suggesting that you are free to choose an attribute for every occurence?

Best regards,
Wolfgang