[clean-list] uniqueness question

[John van Groningen]

Carlos Aya wrote:
>Well, what I want to achieve is a more generic 'update in place' for arrays. For example, to implement something like "v1 += v2" for arrays. My current attempt goes like this ----------------------------------------------------------- . . . addInPlace :: *(a e) .(b e) -> *(a e) | Array a e & Array b e addInPlace arr1 arr2 = updateInPlace arr1 (\v p = v + arr2.[p]) (size arr2) updateInPlace :: *(a e) .(e Int -> e) Int -> *(a e) | Array a e updateInPlace arr1 f maxPos = updateLoop_ arr1 f 0 maxPos updateLoop_ :: *(a e) .(e Int -> e) Int Int -> *(a e) | Array a e updateLoop_ arr1 f pos maxPos | pos == maxPos  = arr1 # (v, arr1) = arr1![pos] = {(updateLoop_ arr1 f (pos+1) maxPos) & [pos] = f v pos} ----------------------------------------------------------- I am getting this error... Overloading error [test1.icl,7,addInPlace]: internal overloading of "lambda [line 8]" could not be solved.

Because + is also overloaded. Adding "| + e" to the type of addInPlace
should fix this.

>which probably displays my ignorance. [You get the idea, this should be a closure with arr2 inside, v comes from the actual value in arr1 at p. See functions below.] But the funny thing is the error with updateLoop_, have a look... Type error [test1.icl,13,updateLoop_]:derived type conflicts with specified type: *(a b) (b -> Int -> b) Int Int -> *(a b) | Array a b *(a b) .(b -> Int -> b) Int Int -> *(a b) | Array a b The two types are identical BUT the function parameter (e Int -> e) has attribute any "." in my signature and _no_ attribute in the inferred type. If I change my signature and remove the uniqueness attribute for f [in updateLoop_ and updateInPlace], it passes. What's wrong here?

Edsko has already explained this.

>John, I read the paper and still don't get it. Could you please provide an example?

f :: *{#Int} Int -> Int
f a i
	# (a0,a) = a![0]
	  a = {a & [0]=a0+1}
	= a.[i]

g1 a
	# h = f a
	= h 0

g2 a
	# h = f a
	= h 0 + h 0

The function h in g1 contains a unique array, and may therefore
only be used once. g1 uses h just once, so is accepted by the typechecker.

g2 tries to use h twice, this is not allowed, because the first call
of f would change the array, then the second call of f gets this updated
array instead of the original array, and the result of the function would
be incorrect.

>..

Kind regards,

John van Groningen