Articles

Understanding Effective Unions in Whiley

The concept of effective union types in Whiley exposes some interesting features worth considering.  In particular, they result in a separation between the readable and writeable view of a type.  But, we’re getting ahead of ourselves!  Let’s start with what exactly effective unions are…

Effective Unions

An effective union is a union type which . . . → Read More: Understanding Effective Unions in Whiley

Flow Typing with Constrained Types

Flow-sensitive typing (a.k.a. “Flow Typing”) is definitely getting more popular these days. Ceylon, Kotlin, TypeScript, Racket, Whiley all support flow typing in some form. Then, of course, there’s Facebook Flow and the list goes on!

Recently, I’ve made some fairly major updates to the internals of the Whiley compiler (basically, redesigning the intermediate language). . . . → Read More: Flow Typing with Constrained Types

Understanding why Union Types are useful

The Whiley programming language uses union types as a way of combining types together.  Here’s a simple example to illustrate:

function indexOf(string str, char c) => null|int: for i in 0..|str|: if str[i] == c: return i // found a match // didn’t find a match return null

Here, the type null|int is a . . . → Read More: Understanding why Union Types are useful

Iso-Recursive versus Equi-Recursive Types

An important component of the Whiley language is the use of recursive data types.  Whilst these are similar to the algebraic data types found in languages like Haskell, they are also more powerful since Whiley employs a structural type system. So, what does all this mean? Well, let’s look at an example:

define IntList as . . . → Read More: Iso-Recursive versus Equi-Recursive Types

Formalising Flow Typing with Union, Intersection and Negation Types

The Whiley language takes an unusual approaching to static typing called flow typing.  This helps to give Whiley the look-and-feel of a dynamically typed language.  The key idea behind flow typing is to allow variables to have different types at different points in a program.  For example, consider the following code written in a . . . → Read More: Formalising Flow Typing with Union, Intersection and Negation Types

Flow Typing for References in Whiley

The Whiley language splits into a fully functional “core” and an imperative “outer layer”.  References and objects do not exist within the functional core.  However, they can exist within the imperative outer layer and are necessary for supporting state and other side-effecting computation.  Here’s a simple example:

define Buffer as ref { [int] items . . . → Read More: Flow Typing for References in Whiley

Termination of Flow Typing in Whiley

Whiley uses flow typing to give it the look-and-feel of a dynamically typed language (see this page for more on flow typing).  In short, flow typing means that variables can have different types at different program points.  For example:

define Node as { int data, Tree left, Tree right } define Tree as null . . . → Read More: Termination of Flow Typing in Whiley

The Whiley Automata Library (WYAUTL)

As part of the upcoming v0.3.10 release of Whiley, I’ve invested considerable effort reimplementing the type system.  This was necessary because, whilst my old implementation generally worked, writing larger programs exposed a lot of issues.  The most interesting aspect of this process is the development of a general-purpose library for representing and manipulating tree . . . → Read More: The Whiley Automata Library (WYAUTL)

Simplification vs Minimisation of Types in Whiley

Recently, I’ve been trying to harden up the implementation of Whiley’s type system. The reason for this is fairly straightforward: bugs in the code often prevent me from compiling correct programs!

In thinking about how to restructure the algorithms I’m using, I realised its important to distinguish simplification from minimisation.  I’ve talked about minimisation . . . → Read More: Simplification vs Minimisation of Types in Whiley

A Semantic Interpretation of Types in Whiley

An interesting and intuitive way of thinking about a type system is using a semantic interpretation.  Typically, a set-theoretic model is used where a type T is a subtype of S iff every element in the set described by T is in the set described by S.

The Semantic Model

The starting point is . . . → Read More: A Semantic Interpretation of Types in Whiley