[clean-list] RE: True Uniqueness Typing Error or Compiler Bug ?

[Fabien Todescato]

Thank you Erik for these enlightening comments,

Your explanation makes sense but I have trouble making it fit with my
current understanding of uniqueness variable and type-checking.

Usually, type variables introduce degrees of freedom, so that for example x
-> x is less restrictive than Int -> Int, and this agrees with the usual
partial order on type terms. That is, x -> x is more general than Int -> Int
because there exists a substitution s such that s(x->x) = Int->Int, namely s
= { x = Int }.

Now, from your explanation it is somehow the reverse with uniqueness
attributes. Indeed, though u:Int -> u:Int = * Int -> * Int with the
substitution u = *, actually the type u:Int -> u:Int is more restrictive
since it requires that both unique and non-unique Int may be manipulated by
the function so typed.

There is a general pattern at work here : uniqueness attributes actually put
constraints on the types, therefore, the more freedom in the constraints on
the type, the less freedom on the type.

I will have to go through the reference manual again to get rid of my
misconceptions about uniqueness typing, I fear.

Again, thank you for your comments.

Best regards, Fabien Todescato

> -----Message d'origine-----
> De:	Erik Zuurbier [SMTP:EZuurbier@Abz.nl]
> Date:	jeudi 23 janvier 2003 10:36
> À:	'clean-list@cs.kun.nl'
> Cc:	'f.todescato@larisys.fr'
> Objet:	True Uniqueness Typing Error or Compiler Bug ?
> 
> Fabien wrote: 
> >Dear Cleaners, I get the following uniqueness typing error from the 2.0.2
> compiler : 
> >Type error [uTypeBug.icl,14,nextSymbol] : specified type 
> >( Char -> Int -> u:File -> u:File) (u:File->u:File) Int u:File -> u:File
> conflicts with derived type 
> >( Char -> Int -> * File -> * File) (* File->* File) Int * File -> * File 
> >which I find quite confusing since the former type can be unified with
> the latter with the substitution u = '*'. 
> 
> 
> My understanding of uniqueness attributes such as u: is that each variable
> can take on two different values, unique or non-unique. That would mean
> that your specified type asserts that the function has two different type
> instantiations:
> 
> ( Char -> Int -> * File -> * File) (* File->* File) Int * File -> * File 
> 
> this is is the one derived by the compiler, and: 
> 
> ( Char -> Int ->   File ->   File) (  File->  File) Int   File ->   File 
> 
> The type checker apparently cannot agree with this latter one. And indeed
> the function's implementation contains fseek and freadc - operations that
> work only on unique files.
> 
> Regards Erik Zuurbier 
>