[clean-list] Re: relationship between uniqueness types and
single-threaded lambda calculus?
megacz at cs.berkeley.edu
Tue Sep 25 07:35:51 MEST 2007
[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
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
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
- 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
More information about the clean-list