[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. 
> 
> Can I write a Clean program with a function that duplicates World?
> 
Clean won't let you duplicate the World. My comment on the mismatch with 
linear logic is aimed more at general uniqueness type systems (e.g. recent 
work by de Vries, Plasmeijer, and Abrahamson such as 
https://www.cs.tcd.ie/~devriese/pub/ifl06-paper.pdf). Sorry for the 
confusion.

-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/48c0cf84/attachment.htm