🚀 go-pugleaf

kff@dentex.tds.kth.se (Karl-Filip Faxen) writes:

>Hello!
>
>Unique types seem related, if not identical, to what Phil Wadler
>calls "linear types". His (and others) work is (as far as I know)
>based on Girard's linear logic, in which assumptions must be used
>exactly once. Thus the type checker guarantees that variables with
>linear types are used exactly once. The major application so far
>seems to have been the array update problem (guaranteeing that
>arrays are used in such a way that array update can safely be 
>implemented without copying).
>
>So, are unique types the same as linear types?

Yes, I believe so.
(Who am I to answer this question? I had never heard of either of them
until they came up here! But from my limited understanding, yes :-)

On the other hand if I were implementing arrays with destructive
update, I would not use exactly what has described as linear types or
unique types.  When we are talking about I/O states, it is not possible
to refer to the same state more than once - once you have invoked some
I/O operation, the state has changed and it may be physically
impossible to return to the old state.  Thus you must issue an error
message if a program tries to use the same I/O state twice. However
with arrays, you *can* refer to them twice - it's just not as efficient
that way. Instead of issuing an error message when an array is used
twice, you should automatically copy the array, perhaps issuing a
warning at most.

-- 
Fergus Henderson             fjh@munta.cs.mu.OZ.AU      
This .signature virus is a self-referential statement that is true - but 
you will only be able to consistently believe it if you copy it to your own
.signature file!