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

Edsko de Vries devriese at cs.tcd.ie
Fri Nov 2 15:51:26 EDT 2007


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


More information about the Haskell-Cafe mailing list