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

[Adam Megacz]

Hello!

After reading Dana Harrington's thesis, I feel that I have a pretty
good handle on the relationship between uniqueness types and linear
logic (as well as the advantages and disadvantages of each).

However, I feel less certain of the comparison between uniquneness
types and the "single-threaded polymorphic lambda calculus" of Guzman
and Hudak [1].  Can anyone shed light on the advantages or
disadvantages of each?

(quick review of STPLC follows)

   It seems that the STPLC offers a new usage mode for "read-only"
   operations on mutable objects (described as "use r" in the paper).
   That is, their array-lookup and array-update functions have type
   
     lookup :: (Array a) -[r]->  Int -[r]-> a
     update :: (Array a) -[ws]-> Int -[r]-> a -[cs]-> (Array a)
   
   In the update function, the "ws" means that the argument is mutated
   (written) and a single reference to it appears as part of the value
   returned by the function.

   The "r" means that the second argument of each function (and the
   first argument of lookup) is examined by the function, but no
   references to it appear as part of the return value.

   The "cs" means that the third argument to update is captured, and a
   single reference to it appears as part of the return value.

   There is one other usage mode known as "cm", meaning the value is
   captured and multiple references to it appear in the return value;
   for example,

     tuple :: a -[cm]-> (a,a)
     tuple x = (x,x)

   Note that all mention of "return value" above applies equally to
   the closure resulting from partial application of a curried
   function.

(end of quick review of STPLC)

It seems that an analogue of STPLC's "r" mode is not present in Clean.
This seems advantageous: STPLC's array lookup function does not need
to return the input array as part of the output (STPLC adds a
sequencing operator), whereas the equivalent "uselect" operation in
Clean does.  This makes array modification code more natural; there is
no need to explicitly sequence two read operations (although read
operations must still be sequenced relative to writes).

Any additional insights would be appreciated!

  - a

[1] Guzman, J.C.; Hudak, P, Single-threaded polymorphic lambda
    calculus. Logic in Computer Science, 1990. LICS '90, Proceedings.,
    Fifth Annual IEEE Symposium on e, Vol., Iss., 4-7 Jun 1990
    Pages:333-343

-- 
PGP/GPG: 5C9F F366 C9CF 2145 E770  B1B8 EFB1 462D A146 C380