Intro to Linear types & Uniqueness types
UIUC CS 421, Summer 2007
Sameer Sundresh <sundresh@uiuc.edu>

Linear types are a way that we can account for operations that have side
effects when performing static type checking on a program.

Say we have a type file_stream, and operations

read_char : file_stream -> char
file_position : file_stream -> int

Just looking at the types, the following two functions should be equivalent:

let reader (fs : file_stream) =
	let c = read_char(fs) in
		(c, file_position(fs));;

let reader (fs : file_stream) =
	let pos = file_position(fs) in
		(read_char(fs), pos);;

reader : file_stream -> char * int

But they're not, because after reading the character from the file stream,
the file position is updated.  The problem is that this isn't reflected in
the types.  Linear types allow us to overcome this problem by marking as
variable as "used" after we have modified what it refers to (for example,
the file pointer, or even things in the real world).

A variable which has a linear type must be used exactly once.
A variable which has a uniqueness type can be used at most once.

read_char : file_stream -> (char * file_stream)
file_position : file_stream -> (int * file_stream)

let reader1 (fs : file_stream) =
	let (c, fs2) = read_char(fs) in
	let (pos, fs3) = read_char(fs2) in
		(c, file_position, fs3);;

reader1 : file_stream -> char * int * file_stream

let reader2 (fs : file_stream) =
	let (pos, fs2) = read_char(fs) in
	let (c, fs3) = read_char(fs2) in
		(c, file_position, fs3);;

reader2 : file_stream -> char * int * file_stream

Now it's easy to tell that the above two functions are not equivalent,
because the calls to file_position and read_char are ordered based on an
output-input dependency (via fs2).  However, it is a bit unwieldy to have to
explicitly pass the state around; some languages, such as Haskell, have
special syntax to make it easier to pass the state around without having to
be as explicit about it.  The core mechanism used to express imperative
(effects-bearing) operations in Haskell is known as a "monad," which is a
bit different from linear types; you can look it up online and read more if
you're interested.