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

[Adam Megacz]

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

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.

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

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

  - a

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