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

Edsko de Vries devriese at cs.tcd.ie
Tue Jun 5 11:51:37 MEST 2007


Hey,

Thanks lethevert for the reference! You are completely right (and so was
Adam's hypothesis about the compiler reasoning about the return type).
At mentioned in that section form the report, if the compiler cannot
conclusively determine that (in the running example) there are no
references to the array as returned by selectx, then the arr is marked
as shared, both in the #! and in the main body of the function. Hence
the uniqueness error. 

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

Thanks for the example! I learned something new today :)

Edsko


More information about the clean-list mailing list