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

[Jonathan Cast]

On Fri, 2007-11-02 at 15:43 -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?
> > 
> 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. 

Ah.  I see.

jcc