[Haskell-cafe] Re: Semantics of uniqueness types for IO (Was: Why
can't Haskell be faster?)
jeff.polakow at db.com
Fri Nov 2 14:41:12 EDT 2007
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".
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...
More information about the Haskell-Cafe