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
_______________________________________________
clean-list mailing list
[email protected]
http://mailman.science.ru.nl/mailman/listinfo/clean-list
