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

[Edsko de Vries]

Hey,

> Could you give a more specific reference (paragraph, etc)?  Also, what
> version of the Clean Report are you reading?  I have version 2.1, and
> it doesn't explain this at all (as far as I can tell).

I checked the manual that's linked to from the Clean manual page:

http://clean.cs.ru.nl/download/Clean20/doc/CleanRep2.0.pdf

The relevant section is 9.4, "Uniqueness and Sharing", p 82.

> But, if it says what I think you're saying it says, then I would
> summarize my comments by saying that uniqueness types have no way of
> expressing "function f cannot capture part of its argument in its
> result" polymorphically, or even monomorphically at arbitrary types.

Yes, I think that is correct. Uniqueness typing doesn't really talk
about "threading" at all. Even if a function has type *a -> *a, the two
a's may be completely unrelated, and there is no way to indicate in the
type whether or not they are. This doesn't really have anything to do
with monomorphism or polymorphism: the type system simply doesn't talk
about threading. 

It's a notion I didn't really understand when I was reading the STPLC
paper, having thought about uniqueness typing for too long :) But I
guess the swap example shows that in fact it may be useful to be able to
indicate this in the type system. Exactly how useful depends on the
application I guess. Maybe folk with more experience actually writing
programs with uniqueness types can offer some comments about this?

> I'm going to think about how to import aspects of STPLC in order to
> extend uniqueness types with this ability.

That could be interesting, let us know how you get on :)

> > Incidentally, the same sort of thing happens in linear logic. From the
> > paper I mentioned before: "We must ensure that u (the let argument)
> > cannot smuggle out any component of x that is linear".
> 
> Um, I doubt this too...  I don't think linear logic treats Int any
> differently than {Int} -- although it does treat the linear version of
> each differently from the exponential version of the same.

Well, that was a literal quote from a paper by Philip Wadler :) In

Linear types can change the world!
Philip Wadler. In M. Broy and C. Jones, editors, Programming Concepts
and Methods, Sea of Galilee, Israel, April 1990. North Holland,
Amsterdam, 1990.
http://homepages.inf.ed.ac.uk/wadler/papers/linear/linear.ps

Section 4 talks about "let*", and the problems and their solutions are
very similar to the ones in Clean. Here is a quote:

 A new form of term is introduced for granting read-only access:

 let! (x ) y = u in v : This is evaluated similarly to a conventional
 let term: first u is evaluated, then y is bound to the result, then v
 is evaluated in the extended environment. But there are three
 differences from a garden-variety let.

He then explains that x must be non-linear (non-unique) in u, even
though it may be linear in v and that u must be fully evaluated before v
(these were the two conditions I had mentioned before). Then there is a
third condition:

 The third is that there are some constraints on the type of x and u. It
 must not be possible for u (or any component of u) to be equal to x (or
 any component of x )-- otherwise, read access to x (or a component of x
 ) could be passed outside the scope of u. This condition is made
 precise below.

 Define the components of a type to be itself and, if it is a base type,
 all components of its immediate components. We will restrict our
 attention to the case where all components of the type of x are base
 types.

 (..some definitions that are hard to typeset in ASCII :)..)

 Let T be the type of x , and U be the type of u. We must ensure that u
 cannot "smuggle out" any component of x that is linear. This is
 guaranteed if no linear component of T has a corresponding nonlinear
 component in U , and if no component of U is a function type.
 (Functions are disallowed since a function term may have x or a
 component of x as a free variable.) If this holds, say that U is safe
 for T .

Edsko