[clean-list] discussing issues of uniqueness typing

[Wolfgang Jeltsch]

Hello,

I'm currently dealing with the paper Uniqueness Typing for Functional 
Languages with Graph Rewriting Semantics.  In this context a question arose 
which I would like to discuss with you.

Before I start, a few words about the notation I use.  I use * to denote 
uniqueness and x to denote non-uniqueness, so * corresponds to \bullet and x 
corresponds to \times in the above-mentioned paper.  I don't give uniqueness 
attributes as superscripts or stacked on top of an arrow, so I write things 
like List*(a), ->* and ->x.

Lets first deal solely with algebraic types.  If a term has a unique type, 
there is at most one reference to it, if it has a non-unique type, there is 
an arbitrary number of references to it.  So it makes sense to have a subtype 
relation which for every n-ary type constructor T states that

	T*(t1, ..., tn) <= Tx(t1, ..., tn)

for arbitrary types t1, ..., tn.

-> is different.  We need a way to specify that a reference to a term of 
functional type is not allowed to be duplicated.  The paper uses * also to 
specify this.  This results in an adapted subtyping rule where the relation

	t1 ->* t2 <= t1 ->x t2

does not hold.

However, I cannot see any reason for not allowing

	t1 ->x t2 <= t1 ->* t2

since I cannot imagine a situation where sharing of function terms can cause 
any problems since functions cannot be updated in place.  If we define * on 
functions to mean "Don't duplicate references." and not necessarily "There is 
only one reference.", I cannot see why such a subtyping inequality should be 
forbidden.

Is there any good reason why this kind of subtyping relationship is not 
allowed?

Best wishes,
Wolfgang