[clean-list] Re: relationship between uniqueness types and single-threaded lambda calculus?

[Edsko de Vries]

Hi Adam,

> This modified version of your program works properly:
> 
>   // just to make sure that no auto-tuple-strictification is going on
>   ::StrictPair a = Sp !Int !a
>   strictPairFst :: (StrictPair a) -> Int
>   strictPairFst (Sp x y) = x
>   
>   // returns a strict pair (a[i],i)
>   selectx :: *{Int} Int -> StrictPair Int
>   selectx x y = Sp (select x y) y
>   
>   // this works
>   swap :: *{Int} Int Int -> *{Int}
>   swap arr i j
>       #!
>          a = Sp (select arr i) i
>          //a = selectx arr i
>          b = select arr j
>       = (update (update arr i b) j (strictPairFst a))
> 
> But if I comment out the definition of "a" and uncomment the line
> after it, the compiler says '"arr" demanded attribute cannot be
> offered by shared object'.

I think you are missing the point of the #! (or, equivalently, of let*).
The reason that you can use "arr" twice in the #! (let*) block consists
of two parts:

  (1) The arr is assumed non-unique within the let* block, and
  (2) The definitions in the let* block must be evaluated before the body

Together, these guarantee referential transparency; (1) guarentees that
no definition in the let* block can modify the arr (because it has a
non-unique type), and (2) guarantees that all these reads happen before
potential writes in the body of the let. I think this is the same in the
STPLC and in uniqueness typing.

Just to be very explicit: the reason that the program with "selectx" is
failing is that you gave selectx a type annotation, requiring it to be
passed a unique array. Since the arr is non-unique within the let* body,
the call to selectx is invalid. However, your annotation to selectx is
too restrictive. The following annotation is valid, and makes either
version of your program pass the typechecker:

selectx :: {Int} Int -> StrictPair Int

Hope that helps,

Edsko