Uniqueness Type - Introduction

Introduction

Uniqueness typing is best explained using an example. Consider a function readLine that reads the next line of text from a given file:

function readLine(File f) returns String return line where String line = doImperativeReadLineSystemCall(f) end end

Now doImperativeReadLineSystemCall reads the next line from the file using an OS-level system call which has the side effect of changing the current position in the file. But this violates referential transparency because calling it multiple times with the same argument will return different results each time as the current position in the file gets moved. This in turn makes readLine violate referential transparency because it calls doImperativeReadLineSystemCall.

However, using uniqueness typing, we can construct a new version of readLine that is referentially transparent even though it's built on top of a function that's not referentially transparent:

function readLine2(unique File f) returns (File, String) return (differentF, line) where String line = doImperativeReadLineSystemCall(f) File differentF = newFileFromExistingFile(f) end end

The unique declaration specifies that the type of f is unique; that is to say that f may never be referred to again by the caller of readLine2 after readLine2 returns, and this restriction is enforced by the type system. 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.