Linear Types for Whiley

[DavePearce]

An interesting question would be to add linear types to Whiley. This could take the form of a linear modifier which, in fact, is very similar to the existing final modifier. The following illustrates some examples:

linear int x = 0
x = 1

The above doesn't compile because the second assignment is not permitted (same as for final).

linear int x
if ...:
   x = 1
else:
   x = 2

The above does compile (same as for final).

linear int x = 0
int y = x

The above does not compile because y is not linear (differs from final). Likewise, as follows:

function id(int a) -> (int b):
    return a

linear int x = 0
int y = f(x)

Again, the above does not compile because a is not linear.

See: The Design and Formalization of Mezzo, a Permission-Based Programming Language, TOPLAS'16.

[DavePearce]

As an interesting point, the following must have linear type:

type l_rec is { linear int field }

Linearity of l_rec is implicit because it contains a field which is itself linear. An interesting question then becomes about this:

type Box<T> is { T field }

At this point, we might want to be able to write Box<linear int> or similar to denote a proper linear item.