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 an "if" expression. When there are two or more code paths that hold a variables 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?

Phi functions have type signatures. Normally these type signatures and the effects of their applications may be inferred without extra work from the programmer. However, there are some cases where the programmer may want to customize the behavior of the phi function.

To permit this customization, LSTS provides a special type called Phi. When the phi function sees a Phi type it knows that the programmer is asking for extra control.

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

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;

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;