[Haskell-cafe] Re: Semantics of uniqueness types for IO
(Was: Why can't Haskell be faster?)
jonathanccast at fastmail.fm
Fri Nov 2 15:13:09 EDT 2007
On Fri, 2007-11-02 at 14:41 -0400, Jeff Polakow wrote:
> Just a bit of minor academic nitpicking...
> > Yeah. After all, the "uniqueness constraint" has a theory with an
> > excellent pedigree (IIUC linear logic, whose proof theory Clean uses
> > here, goes back at least to the 60s, and Wadler proposed linear
> > for IO before anybody had heard of monads).
> Linear logic/typing does not quite capture uniqueness types since a
> term with a unique type can always be copied to become non-unique, but
> a linear type cannot become unrestricted.
Can I write a Clean program with a function that duplicates World?
> As a historical note, the first paper on linear logic was published by
> Girard in 1987; but the purely linear core of linear logic has
> (non-commutative) antecedents in a system introduced by Lambek in a
> 1958 paper titled "The Mathematics of Sentence Structure".
OK then. Correction accepted.
More information about the Haskell-Cafe