Re: Semantics of uniqueness types for IO
Hey, Just to continue the academic nitpicking.. :-)
Linear logic/typing does not quite capture uniqueness types since a term with a unique type can always be copied to become non-unique, but a linear 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). By contrast, in uniqueness typing we certainly don't want to allow treat a term with a non-unique type as having a unique type, but we *may* want to allow to treat a term with a unique type as having a non-unique type (as you mention). However, you have to be very careful when you do that: if you allow to treat functions with a unique type as having a non-unique type, you loose all uniqueness guarantees unless you indicate in the type of the term whether or not the function has any unique elements in its closure. If you don't, you could for example construct a term that duplicates unique elements using dup x = (\f -> (f _|_, f _|_)) (\y -> x) (which would get type "forall a, unique a to pair of unique a's" if you allow to copy unique functions and then apply them). Edsko
Just to continue the academic nitpicking.. :-)
Linear logic/typing does not quite capture uniqueness types since a term with a unique type can always be copied to become non-unique, but a
Hello, linear
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. -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.
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. Sorry for the 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.
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.
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
participants (2)
-
Edsko de Vries -
Jeff Polakow