[Haskell-cafe] Re: Semantics of uniqueness types for IO

[Edsko de Vries]

Hey,

On Fri, Nov 02, 2007 at 04:02:12PM -0400, Jeff Polakow wrote:
> Hello,
> 
> > I think you mean 
> > 
> >     !U -o U 
> > 
> > is a theorem. The converse is not provable. 
> >
> Oops... I should read more carefully before hitting send. 

No, you were right, I was wrong :) I get confused about the syntax
sometimes :) Anyway,

  !U -o U

is indeed a theorem of linear logic (with the interpretation I gave in
my previous email), and we certainly do not want to allow this theorem
in a uniqueness type system. 

The main point I wanted to make is that in uniqueness typing, it may
seem that we can allow the converse of this theorem (and allow to treat
terms with a unique type as having a non-unique type), but that it is
dangerous to do so unless you take the elements in function closures
into account.

Edsko