Articles

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

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

Type Aliasing in Java?

A problem I often encounter in Java is that I want to say “these two things are the same”, but Java won’t let me. Suppose I want to maintain an int[] array which is always sorted in my program. So, whenever I get one of these things, I can rely on it being sorted. Here’s . . . → Read More: Type Aliasing in Java?

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

Regular Tree Automata

In my quest to understand the theory of recursive types in more detail, the notion of regular tree languages and [[Tree automaton|Tree Automata]] has cropped up.  These have been used, amongst other things, for describing [[XML schema|XML schemas]].  They are also useful for describing recursive types as well!

A nice example of a regular . . . → Read More: Regular Tree Automata

Implementing Structural Types

Introduction

Over the last few months, I’ve been working on the type system underpinning Whiley.  A key feature is the use of [[Structural type system|structural typing]], rather than [[nominal typing]], and I’ve blogged about this quite a bit already (see [1][2][3][4]).  Over the weekend, I finally found time to work through all my thoughts . . . → Read More: Implementing Structural Types

Minimising Recursive Data Types

Following on from my previous post about structural subtyping with recursive types, a related problem is that of minimising recursive types. Consider this (somewhat artificial) example:

define InnerList as null | { int data, OuterList next } define OuterList as null | { int data, InnerList next } int sum(OuterList list): if list ~= . . . → Read More: Minimising Recursive Data Types

A Problem with Structural Subtyping and Recusive Types

One problem causing me a headache is how to implement [[Structural type system|structural subtyping]] for [[recursive data type|recursive types]] (which I first blogged about here). The following example illustrates the basic idea:

define Link as { int data, LinkedList next } define LinkedList as null | Link LinkedList f(Link list): return list

This is . . . → Read More: A Problem with Structural Subtyping and Recusive Types