Articles

On Memory Management and Rust

Rust is definitely one of the more interesting new programming language I’ve come across recently. Memory management is definitely Rust’s “thing”, and the language wants to have its cake and eat it (so to speak). That is, Rust wants safe memory management without garbage collection. This is no easy task, and Rust delivers a . . . → Read More: On Memory Management and Rust

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

Groovy 2.0 uses Flow Typing!

Groovy 2.0 has just been released, and it contains something rather interesting … optional flow typing!  For those who don’t know much about the language, Groovy is a JVM-based dynamically typed language which is similar to Java, but more compact.  And, being dynamically typed means that there’s no need for any cumbersome type declarations.

. . . → Read More: Groovy 2.0 uses Flow Typing!

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

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 Subtyping Gotcha

An interesting issue with the following piece of code has recently come to my attention:

define Queue as process { [int] items } int Queue::get(): item = this.items[0] this.items = this.items[1..] return item void Queue::put(int item): this.items = this.items + [item] Queue ::Queue(): // following line should be invalid return spawn { items: [] . . . → Read More: A Subtyping Gotcha

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