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

[Jeff Polakow]

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. 

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".

-Jeff


---

This e-mail may contain confidential and/or privileged information. If you 
are not the intended recipient (or have received this e-mail in error) 
please notify the sender immediately and destroy this e-mail. Any 
unauthorized copying, disclosure or distribution of the material in this 
e-mail is strictly forbidden.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071102/e11a7ba2/attachment-0001.htm