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

[Edsko de Vries]

Hi Adam,

I had a quick read through the paper you mentioned. However, since that
was the first time I read about the STPLC, I find it hard to compare it
to uniqueness typing. I agree that one difference is that the example
they give in the paper:

swap! a i j = 
  let* x = lookup a i
       y = lookup a j
  in update! (update! a i y) j x

cannot be typed in Clean. However, I'm not sure if this is due to the
lack of the "r" mode Instead, I would venture that this is due to the
absence of a "let*" construct in Clean.  I'm not sure why it isn't there
actually, and it would be relatively straightforward to add it (I might
just do that in the system I'm proposing :) Clean *does* take the
evaluation order into account in some cases however; in particular, in
conditionals. For example, if we have

is_blank :: Array -> Bool
clear :: *Array -> *Array

then the following is a well-typed Clean program:

  \arr. if (is_blank arr) arr (clear arr)

even though there are three references to "arr", this program is
well-typed, because the conditional must be evaluated before both
branches (and is_blank only requires a non-unique array), and then only
one of the two branches will be evaluated. Note that "is_blank" does not
return any array.

But I have to admit I'm not 100% sure about the three different
properties they mention in the paper and all their permutations - it
seems to be that that at least is one advantage of uniqueness typing -
less properties to think about :)

Another thing I'm not sure about is exactly how polymorphic their
calculus is, but perhaps you can tell me: for example, in STPLC, what
would be the type of 

 \x. x
 \x. \y. x
 \f. \x. f x

It may be interesting to compare the types of those functions to their
types in Clean (and maybe to the types in my own uniqueness system :)

Edsko