If a value has a unique type, a function applied to it can be optimized to update the value in-place in the object code.
And since readLine2 does not return f itself but rather a new, different file object differentF, this means that it's impossible for readLine2 to be called with f as an argument ever again, thus preserving referential transparency while allowing for side effects to occur.
Uniqueness types are implemented in functional programming languages such as Clean, Mercury, SAC and Idris.
A compiler extension has been developed for the Scala programming language which uses annotations to handle uniqueness in the context of message passing between actors.
[2] Linearity and uniqueness can be seen as particularly distinct when in relation to non-linearity and non-uniqueness modalities, but can then also be unified in a single type system.