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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
