Dr. David J. Pearce

Type Checking in Whiley goes Both Ways!

Type checking in Whiley is a curious thing as it goes both forwards and backwards. This is sometimes referred to as bidirectional type checking (see e.g. here and here). This is surprisingly useful in Whiley (perhaps because the language has a reasonably unusual feature set).

Backwards Typing

Type checkers normally work in a backwards (or bottom up) direction. That is, they start from leaves of the abstract syntax tree and work upwards. Typing a statement like xs[i] = ys[i] + 1 (when xs and ys have type int[]) might look something like this:

Illustrating types being pulled up the AST of an expresion.

They key here is that types have to agree (modulo subtyping), otherwise we have a type error.


As a general approach, backwards typing works well in most cases. But, there are some limitations when applying this to Whiley:

Forwards Typing

A key observation is that, in many situations, we already have concrete type information available. For example, consider this declaration:

u8[] bytes = [1,2,3]

We can type this in a forwards (or top down) direction by “pushing down” from the declared type u8[] of bytes. This means we give [1,2,x+1] the type u8[] and then push u8 into each of the subexpressions 1, 2, and x+1, as follows:

Illustrating types being pushed down the AST of an expresion.

Bidirectional Typing

Bidirectional typing, as the name suggests, is about mixing forwards and backwards typing. But, you might wonder why we don’t just use forwards typing all the time? Well, the answer is pretty simple: in some cases, you simply cannot use forward typing. Therefore, in such cases, we default back to backwards typing. The following illustrates such an example:

function headerOf<T>(Node<T> n, Node<T> c) -> bool:
  return n == h1(c)

The issue is that the type being pushed down from the return statement into its expression is bool, but this provides no useful information about the operand types for ==. In otherwords, when typing n we simply don’t have a type to push down. What we can do instead, however, is “pull up” the type from n and then push that down into h1(c).

In the example above, there wasn’t a type we could push down into the subexpression. So, we didn’t have any choice but to pull up instead. However, there are situations where we have a type to push down — but it is undesirable to do so. The following illustrates:

u8[] items = [0,1,2]
u16 item = items[0]

In the above, we can push u16 into items[0] and, based on this, push u16[] into down into the access of items. However, this then forces a coercion of the entire items array from u8[] to u16[]. This is less than ideal since we only want to access (and, hence, coerce) one element from items. Therefore, when typing items[0] its preferable to pull the type of items up (as this corresponds to its natural representation). This then forces a coercion from u8 to u16 at that point, rather than further down the tree.


Bidirectional typing allows for more concise and elegant code than the typical bottom up approach. This has considerably improved the user experience when writing Whiley code. However, it is worth noting that bidirectional type checking algorithm now used in Whiley is considerably more involved than the original bottum up algorithm.


A few useful papers on the subject: