Articles

Flow Typing

Whiley takes a novel approach to static typing called flow-sensitive typing or just flow typing for short.  This aims to give the flexibility of a [[Type system#Dynamic_typing|dynamically typed language]], with the guarantees of a [[Type system#Static_typing|statically typed language]].  The technique is adopted from flow-sensitive [[program analysis]], and allows variables to have different types at different points.  Furthermore, local variables do not have declared types but, instead, their type is inferred from assigned expressions.

Variable Retyping

The following demonstrates Whiley’s flow-sensitive type system:

define Circle as {int x, int y, int radius}
define Rectangle as {int x, int y, int width, int height}
define Shape as Circle | Rectangle

real area(Shape s):
    if s is Circle:
        return PI * s.radius * s.radius
    else:
        return s.width * s.height

Here, a Shape is either a Rectangle or a Circle (which are both record types). The type test s is Circle (similar to an instanceof test in Java) determines whether s is a Circle or not. Unlike Java, Whiley automatically retypes s to have type Circle (resp. Rectangle) on the true (resp. false) branches of the if statement. Thus, there is no need to explicitly cast s to the appropriate Shape before accessing its fields.

Implicit Declaration

Statically typed languages typically require variables be explicitly declared. Compared with dynamically typed languages, this is an extra burden for the programmer, particularly when a variable’s type can be inferred from assigned expression(s). In Whiley, local variables are never explicitly declared, rather they are declared by assignment. The following illustrates:

define err as {string msg}

int|err average([int] items):
    if items == []:
        return {msg: "empty items"}
    v = 0
    for i in items:
        v = v + items[i]
    return v / |items|

Here, items is a list of int, whilst |items| returns its length. If items is empty, the above function returns an error message; otherwise, it averages the elements of items. The variable v is used to accumulate the sum of all elements in the list. Variable v is declared by the assignment from 0 and, since this has type int, v has type int after the assignment.

Example: Nullable Types

Nullable references have proved a significant source of error in languages such as Java, which  do not distinguish nullable from non-null references. Whiley’s flow-sensitive type system naturally handles this problem.  For example:

null|int indexOf(string str, char c):
...

[string] split(string str, char c):
    idx = indexOf(str,c)
    if idx is int:
        // matched an occurrence
        below = str[0..idx]
        above = str[idx..]
        return [below,above]
    else:
        return [str] // no occurrence

Here, indexOf() returns the first index of a character in the string, or null if there is none.  The type null|int is a [[Union (compuer_science)|union type]], meaning it is either an int or null.

In the above example, Whiley’s flow-sensitive type system seamlessly ensures that null is never dereferenced.  This is because the type null|int cannot be treated as an int. Instead, we must first perform a runtime type test to ensure it is an int.  Whiley automatically retypes idx to int when this is known to be true, thereby avoiding any awkward and unnecessary syntax (e.g. casts).

Example: List Length

The following function for calculating the length of a LinkedList data type provides another useful example:

define LinkedList as null | {int data, LinkedList next}

int length(LinkedList l):
  if l is null:
    return 0
  else:
    return 1 + length(l.next)

Here, we again see how flow typing gives a nice solution. More specifically, on the false branch of the type test l is null, variable l is automatically retyped to {int data, LinkedList next} — thus ensuring the
subsequent dereference of l.next is safe. No casts are required as would be needed for a conventional imperative language (e.g. Java), making the code simpler and more elegant.