Linear types are an interesting idea.
I really liked the way that each transformation of the file was a separate File object, reminded me of functional style immutable data structures where each transformation returns a new structure.
I really liked the way that each transformation of the file was a separate File object, reminded me of functional style immutable data structures where each transformation returns a new structure.
They look very similar on the surface and are sometimes confused. The paper Linearity and Uniqueness: An Entente Cordiale[2] goes into depth on the differences - but it basically boils down to - Uniqueness is about the history of some value - a contract that asserts it has not been aliased in the past. Linearity is about the future of the value - a contract that it must be consumed exactly once, from this point onward.
The benefit of uniqueness types is that it enables us to perform in-place mutation, because we know that nowhere else is this value aliased. The benefit of linear types is to guarantee proper cleanup. The two systems complement each other, and we can have types which are both unique and linear - steadfast types.
Austral doesn't have uniqueness types as such, but Capabilities are used to fulfil the same purpose. Because capabilities must be created from other capabilities, they're unforgeable - so we can design types that encapsulate a capability which in effect, ensures their uniqueness, but it's a bit more cumbersome than having uniqueness as a property of the language. Granule has both systems built in - uniqueness and linearity - but it doesn't support types which are both - they have to begin unique and be made into linear values.
[1]:https://wiki.clean.cs.ru.nl/download/html_report/CleanRep.2....
[2]:https://granule-project.github.io/papers/esop22-paper.pdf