[Haskell-cafe] Re: Semantics of uniqueness types for
IO (Was: Why can't Haskell be faster?)
jonathanccast at fastmail.fm
Fri Nov 2 15:44:39 EDT 2007
On Fri, 2007-11-02 at 15:43 -0400, Jeff Polakow wrote:
> > > Just a bit of minor academic nitpicking...
> > >
> > > > Yeah. After all, the "uniqueness constraint" has a theory with
> > > > excellent pedigree (IIUC linear logic, whose proof theory Clean
> > > > 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
> > > term with a unique type can always be copied to become non-unique,
> > > 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
Ah. I see.
More information about the Haskell-Cafe