Records

Whiley provides record types (similar to those found in JavaScript) for hierarchically structured data (a.k.a. algebraic data types). The following illustrates the main idea:

void System::main([string] args):
    p = {x:1, y:1}
    z = p.x

Here, we see variable p has a record type with two fields, x and y, which can be accessed using the “.” operator.  Generally speaking, it’s more elegant to use the define operator, like so:

// parser state
define state as { string input, int pos }

// parse whitespace!
state parseWhiteSpace(state st):
  while st.pos < |input| && st.input[st.pos] == ' ':
    st.pos = st.pos + 1
  return st

We can also define record types recursively, which is important for creating composite data-structures.

define tree as {tree lhs, tree rhs} | int

void System::main([string] args):
    tree t2 = 1
    tree t2 = {lhs: t1, rhs: 2}

This example shows several features: firstly, tree is a recursively defined data type which corresponds to some kind of binary tree; secondly, the choice operator “|” defines a data type whose variables can take on either type (a.k.a. union types). In such a situation, we can use the is operator (similar to Java’s instanceof) to distinguish the actual type of a variable:

int eval(tree x):
    if x is int:
        // type of x now int
        return x
    else:
        // type of x now { tree lhs, tree rhs }
        return eval(x.lhs) + eval(x.rhs)

We can see here another useful feature offered by Whiley: flow-sensitive types.  This means the type of a variable can vary at different points within a function.  In the above example, the type of x is adjusted accordingly when x is int is known to be true and, similarly, when it is known to be false.