[Haskell-cafe] Re: Semantics of uniqueness types for IO
jeff.polakow at db.com
Fri Nov 2 16:16:30 EDT 2007
> > 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.
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...
More information about the Haskell-Cafe