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

[Jeff Polakow]

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. 
> 
> This is of course completely wrong. 
> 
This is embarrassing... I was right the first time.

    !U -o U 

is a theorem in linear logic. It can be read as given infinitely many U, I 
can get one U.


    U -o !U 

is not a theorem in linear logic. It can be read as given one U, I can get 
infintely many U.


Sorry about the continued noise.

-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/2fb3d0b0/attachment.htm