[Haskell-cafe] Re: Semantics of uniqueness types for IO
Edsko de Vries
devriese at cs.tcd.ie
Fri Nov 2 16:22:34 EDT 2007
On Fri, Nov 02, 2007 at 04:02:12PM -0400, Jeff Polakow wrote:
> > 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
More information about the Haskell-Cafe