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

Jeff Polakow jeff.polakow at db.com
Fri Nov 2 15:59:44 EDT 2007


> Just to continue the academic nitpicking.. :-)
> > Linear logic/typing does not quite capture uniqueness types since a 
> > with a unique type can always be copied to become non-unique, but a 
> > type cannot become unrestricted. 
> Actually, that isn't quite accurate. In linear logic, a term with a
> non-linear type can always be regarded as having a linear type, i.e.
>   U -o !U
> is a theorem (my favourite reading of this theorem is "if you have an
> unlimited supply of bank notes, then you also have a single one"). The
> implication in the opposite direction is a falsity (from the fact that
> we have a single bank note, we cannot decude that we have an unlimited
> supply).
I think you mean

    !U -o U

is a theorem. The converse is not provable.

In any case, I think we are saying the same thing.


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/ed40b259/attachment-0001.htm

More information about the Haskell-Cafe mailing list