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

[Edsko de Vries]

Hi,

Just a little node:

> The summary/comparison I was looking for would go something like this:
> the most easily identifiable difference between the systems is how
> they prevent a mutable value from "hiding" in a let*-bound closure.
> 
>   - Wadler's "smuggling" restriction prohibits let*-bound values from
>     being of functional type, being polymorphic, or having
>     subcomponents which are mutable values.  Clean appears to be using
>     this criteria.
> 
>   - STPLC weakens this restriction to merely prohibiting let*-bound
>     values from being of functional type (they may still be
>     polymorphic over first-order types) at the cost of a somewhat
>     more complex type system.
> 
>   - Edsko de Vries's type system appears to lift *all* of the
>     restrictions, so long as you "thread through" any mutable (ie
>     unique) values into a component of the return value.

I'm not sure the last point is valid. My system (so far, at least) does
not deal with this problem at all. If you like: I don't support a 'let*'
construct. A let* construct could be added, but similar 'smuggling'
rules that Wadler or Clean uses must be in place.

Edsko