In Encore, an affine type is defined by an affine (mode) annotation,
lin, followed by a type. For instance:
def readLine(f: read File): read String val f2 = f f2.readLine() end
The formal arguments of this function states that
readLine takes a
File which may have aliases (and can be aliased) and returns a
String that can be aliased as well, since it has the
read annotation. In Encore, the
read annotation also implies that the variable pointer,
f, cannot modify to what it points to (similar to
const in C language).
If we modify the function to:
def readLine(f: lin File): read String var f2 = f f2.readLine() end
lin annotation guarantees that the
File has to be treated linearly – no aliasing is allowed. The type system forbids aliasing and the program above is rejected because
f2 is an alias of
f. Let’s re-write the program so that it typecheks:
def readLine(f: lin File): read String var f2 = consume(f) f2.readLine() end
This new version typechecks, although it may seem as if
f2 is aliasing
f. Nonetheless, the
consume keyword nullifies
f and the assignment makes
f2 to be the only one with access to the contents of the file.
Why are linear references important?
For parallel and concurrent languages, a linear reference guarantees that the user of the reference is the only one who has access to it and cannot be affected by (nor affect) other threads – guarantees data-race freedom and runtime thread-local reasoning.
In a functional setting (and functional abstractions), the runtime has enough information to do in-place updates. In the beginning of the 90s (maybe a bit earlier), this was mentioned quite often in the literature but there was no work that further developed the idea. Martin Hoffman used it for the first time in his paper “A Type System for Bounded Space and Functional In-Place Update” in ESOP’00.
Linear references are important for the Encore language because Encore has many different abstractions to express concurrency and parallelism: actors and tasks, hot objects and ParT types. My current work focuses on formalising the ParT types in an affine type system. Afterwards, ParT types will use this optimisation to save memory and some other optimisations that I dare not to comment on until I know for sure that they do work.