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

[Adam Megacz]

[epilogue to a very old thread]

Edsko de Vries <devriese at cs.tcd.ie> writes:
> At this point (not knowing much more about STLPC than I did two days
> ago) I would say: have a close look at polymorphism. Exactly how
> polymorphic is the STPLC?

My confusion on this issue has been cleared up, and I figured I'd post
what I learned "for the record" in case anybody else wonders the same
thing.

The author of the STPLC paper (Dr. Guzman) was kind enough to answer
my many questions and provide a copy of his thesis.  I'm quite
embarrassed to admit that I had completely overlooked the fact that
his type system requires that values bound in let* have first-order
type.  Once I took that into account, things started to make a lot
more sense.

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.

Thanks again to everybody who put up with my questions and overall
confusion.

  - a