🚀 go-pugleaf

 >>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. 
 >
 >Which brings up the question... if linear logic insists that assumptions be
 >used exactly once, does a language with linear types insist that linear
 >variables be used exactly, as opposed to at most, once? What breaks if you
 >just insist that variables with "linear" types be used at most
 >once---"single threading"? (Is it some sort of strictness that breaks?)
 >
 >Jeremy (a linear novice)

The philosophy behind the development of Linear logic concerns control over
the use of resources. A resource, e.g. an argument to a function, can be used
0, 1 or many times. Only if we restrict its use to exactly once do we achieve
explicit control over its use such that, e.g. we can automatically reclaim the
resource when it is finished with. Relaxing the notion of "linearity" to at
most once means that this control is lost as much as if we had no linearity
at all. The idea proposed above is more akin to "sticky" reference counting.

Simon Courtenage		Email: scourten@uk.ac.ucl.cs
Dept of Computer Science
University College London
London WC1E
England