Type System

Statically typed programming languages (e.g. [[Java (programming language)|Java]], C\#, C++, etc) lead to programs which (generally speaking) are more efficient and have fewer errors. At a minimum, static typing forces some discipline on the programming process by ensuring, for example, that at least some documentation regarding acceptable function inputs is provided. However, statically typed languages are generally considered to be verbose, and have faced fierce criticism as a result.  In contrast, dynamically typed languages are generally more flexible in nature, which helps reduce overheads and increase productivity.

The Whiley language attempts to bridge the gap between static and dynamic typing by providing a static type system which is both concise and flexible.  This is done with two key features:

  1. Flow-Sensitive Typing — this allows variables to have different types at different points.  and to be declared implicitly from assigned expressions.
  2. Structural Subtyping — this approach to subtyping departs from the more common “nominal typing”, by allowing subtyping between types with different names, but the same structure.

Whilst we are not aware of any other language which uses flow-sensitive typing, a few  languages do structural subtyping (e.g. Scala).