[clean-list] uniqueness attributes of data constructors

[Wolfgang Jeltsch]

Am Montag, 22. August 2005 13:25 schrieben Sie:
> 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,

This makes the situation even more strange.  According to "Uniqueness Typing 
for Functional Programming with Graph Rewriting Semantics" as well as the 
"Clean Version 2.0 Language Report", all occurences of T in the type of C 
should be attributed with the same attribute variable.

> 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.

What happens if you modify the above type declaration for f to this:

	f :: *(T .a) -> .a

As it looks currently, f1 and f2 will still have type .(T .a) -> .a) which 
would be bad, as far as I can see, since this would allow f to be applied to 
non-unique arguments which f is not intended to be applied to.

> [...]

Best regards,
Wolfgang