# Introduction to affine types in Encore

Published:

An affine type system allows either an unlimited number of aliases or no aliases at all. The Encore language has a more powerful type system [1] [2] that can encode affine types.

In Encore, an affine type is defined by an affine (mode) annotation, read or lin, followed by a type. For instance:

def readLine(f: read File): read String
val f2 = f
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
end


the 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)

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.