[clean-list] uniqueness question

[Carlos Aya]

Thanks Edsko and John for your explanations.

Certainly I had a big misunderstanding in regards to unification and uniqueness. In a signature like

    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}

Although f certainly appears twice, I thought that the don't care attribute in .(e Int -> e) was going to be resolved by the compiler saying "well, s/he doesn't care, but I know is not unique, so let's _instantiate_ that unknown variable with non-unique". I was wrong.

For completeness, let me c&p the working solution,
****************************************************
module test1

import StdArray, StdInt, StdReal, StdClass

Start :: {#Real}
Start = addInPlace v1 v2
where
    v1 :: .{#Real}
    v1 = {1.0, 2.0, 3.0}
    v2 :: .{#Real}
    v2 = {0.0, 2.0, 4.5}

addInPlace :: *(a e) .(b e) -> *(a e) | Array a e & Array b e & Arith e
addInPlace arr1 arr2 = updateInPlace arr1 f (size arr2)
where 
    f v p = v + arr2.[p]

updateInPlace :: *(a e) (e Int -> e) Int -> *(a e) | Array a e
updateInPlace arr1 f maxPos = updateLoop_ arr1 f 0 maxPos
where
    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 think I am ready to understake my challenge, a simple in-place matrix library.

Kind regards
Carlos
 



----- Original Message ----
From: Edsko de Vries <edskodevries at gmail.com>
To: Carlos Aya <carlosayam at yahoo.com.au>
Cc: John van Groningen <johnvg at cs.ru.nl>; clean-list at cs.ru.nl
Sent: Tue, 17 November, 2009 9:10:56 PM
Subject: Re: [clean-list] uniqueness question

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


      __________________________________________________________________________________
Get more done like never before with Yahoo!7 Mail.
Learn more: http://au.overview.mail.yahoo.com/