[clean-list] uniqueness question

[Edsko de Vries]

Hi Carlos,

On 17 Nov 2009, at 01:13, 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} 
> 
> -----------------------------------------------------------

Right, so this is an example of what John was talking about. Functions are treated special in Clean (little tongue in cheek: some might argue too special [1]). A unique function cannot be coerced to a non-unique function. Suppose that in the lambda expression you create in addInPlace, you don't just read from arr2 but you write to it. Then we have a closure (a partially applied function) with a unique element (arr2) in its closure. Clearly, this function should only be executed once if we want to have referential transparency - if we execute it twice, then the first execution modifies the array, and then the second execution starts with a *different* array.

Since updateLoop executes f more than once, f must be non-unique (hence the type that Clean has inferred).

Since f must be non-unique, the function that you pass it in addInPlace must also be non-unique. As a consequence, arr2 must be non-unique in addInPlace -- even though you only read from it. I think you won't be able to get around that even with a strict-let-before (but I'm not 100% sure) -- I'm guessing you need a more powerful type system (such as observer types) to be able to do that. (You might however be able to provide a wrapper function that accepts a unique arr2, and then calls addInPlace, since unique arrays are coercible to non-unique arrays).

> John, I read the paper and still don't get it.
> Could you please provide an example? Also, it seems to suggest that the
> types of
> f :: *a .b -> *a
> and
> g :: .b *a -> *a
> could be treated differently as in the last one only the last parameter
> is unique and therefore there is no risk in creating a partial
> application that violates single threaded semantics. Am I right? Is it
> like that in Clean?

Note that the "dot" does not mean non-unique, but rather means "there is a uniqueness variable here that I don't care to name". Your types of f and g expand to

f :: *a u:b -> *a
g :: u:b *a -> *a

To indicate non-unique, you use no annotation at all:

f :: *a b -> *a
g :: b *a -> *a

If we assume the latter definition, then yes, there is a difference. An application (f x) must be applied to a unique x, and threfore will be a partially applied function with a unique element in its closure -- that is, it will be a unique function that can only be applied once. Conversely, (g x) will be applied to a non-unique x and is therefore not subject to such a contraint.

Hope that helps. You can find much more information about uniqueness typing (and more examples) in Section 3.2 of [1]. It also discusses the above problem in great depth.

Edsko

[1]. Making Uniqueness Typing Less Unique, Edsko de Vries, PhD Thesis, Trinity College Dublin, Ireland