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

Type Checking in Whiley goes Both Ways!

submited by

Style Pass

2022-06-21 21:30:08

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).

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:

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

(Sizing). Variables of type int in Whiley can hold arbitrary sized integers and, because of this, backwards typing can lead to inefficiency. Consider this:

Under the backwards typing scheme, the constant 124 is given type int. That means, under-the-hood when the constant is created, we’ll allocate space for an arbitrary sized integer and give it the value 124. Then, we’ll immediately coerce it to a u8 causing a deallocation. It would be much better if we automatically determined the type of 124 was u8 rather than int. Note, one way to solve this is with specific notation for constants (e.g. 124u8 in Rust) — however, bidirectional typing is more elegant.