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

[Adam Megacz]

Edsko de Vries <devriese at cs.tcd.ie> writes:
>> > 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... 

>  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.

I stand corrected!

Additionally, it is very useful to have a more formal explanation of
what's going on here, so that we can at least say "Clean is doing what
Phil Wadler's paper talks about".

Although, with all due respect to Prof. Wadler, I think this form of
the "smuggling restriction" may become problematic in large or very
polymorphic programs.  I'll try to finish working out my thoughts on
how to use your boolean variable approach to get a better definition
of "does not smuggle".

  - a

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