[Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why can't Haskell be faster?)

[Jonathan Cast]

On Fri, 2007-11-02 at 14:41 -0400, Jeff Polakow wrote:
> 
> Hello, 
> 
> 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
> types
> > 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.

jcc