Phi Types

Phi (ϕ) Types are a generalization of the concept of linear typing to permit more programmer customization. Phi Types get their name from the Phi function in Static Single Assignment form.

What is a Phi function in SSA?

Static Single Assignment form only allows variables to be assigned to once, hence the name. When an assignment happens, a new variable version must be created to hold the value. However, this causes a slight problem when dealing with branching conditionals such as "if" expressions. When there are two or more code paths that hold a variable's value, the different variable versions must be merged back into one. To accomplish this, a phi function is used to logically merge variable versions.

Consider the following code.

let x = 5;

if condition {
   x = 4;
};

Rewriting this code in Static Single Assignment will give versions to each assignment.

let x#1 = 5;

if condition {
   x#2 = 4;
}

x#3 = ϕ(x#1, x#2);

What is a Phi Type?

SSA assignment creates new variables, which can also have new types. LSTS provides a special Phi type which allows direct customization of new SSA types.

The special interactions of Phi types are limited to transitions and merges. A Phi transition describes a change to a type signature during an SSA assignment. A Phi merge describes the possible behaviors during Phi function application.

What is an example of Phi Typing?

A phi type can be declared with the phi tag during type declaration.

type phi FileState = Open | Closed;

The fclose function is an example of a Phi transition that changes state from FileState::Open to FileState::Closed.

let fclose(file: File+Phi<FileState::Open,FileState::Closed>): U32;

When fclose is called, it changes the state of its first argument.

let fp = fopen("test.txt", "r");
# fp#0 : File + Phi<12345,FileState::Open>

fclose(fp);
# fp#1 : File + Phi<12345,FileState::Closed>

To compliment this behavior a programmer may also define the permissible merges of FileState.

let phi(left: FileState::Open, right: FileState::Open): FileState::Open;
let phi(left: FileState::Closed, right: FileState::Closed): FileState::Closed;

Now the programmer cannot create a state where a file may be open or closed but impossible to determine which.

Phi types can also be used during specialization. For example, a programmer can declare that open files should automatically be closed when they go out of scope.

let del(fp: File+Phi<FileState::Open>): Nil = fclose(fp);