Documentation

Articles

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

Whiley v0.3.10 Released!

Well, it’s been a tough slog.  But, finally, we have a new release of Whiley!!  The main thing that’s improved over the past few weeks is the underlying type implementation.  This was causing problems before, as programs which should type-check were failing and vice-versa.  To resolve this, the type system has been reimplemented from . . . → Read More: Whiley v0.3.10 Released!

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

The State of Whiley

The aim of this post is simply to list the main outstanding issues with the design and implementation of Whiley.  This is primarily for my own purposes, in order to help me focus my efforts and to ensure I don’t forget something important.

Syntax

Deciding upon the language syntax is obviously the highest priority . . . → Read More: The State of Whiley

Implicit Coercions in Whiley

The issue of implicit coercions in Whiley is proving to be a particularly thorny issue.  The following motivates why (I think) coercions make sense:

real f(int x, real y): return x + y real g(int x, int y): return f(x,y)

I believe the above should compile without error.  However, this requires an implicit coercion . . . → Read More: Implicit Coercions in Whiley

Regular Tree Automata

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

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

On the Duality of Types: the Ideals versus the Reals

I’ve been working hard over the last few weeks on the next release of Whiley, which should be out soon.  However, I’ve got myself into a little bit of a pickle over the type system (again).  I want the type system to be simple and easy to use, but at the same time efficient . . . → Read More: On the Duality of Types: the Ideals versus the Reals

Design by Contract is Most Requested Feature?

Thanks to Alex Potanin for pointing this out to me … it seems that Design by Contract is the most requested enhancement to the Java language.  You can find the list of the top 25 RFEs here.  A nice quote from the feature description:

I find it a shame that all the requests for . . . → Read More: Design by Contract is Most Requested Feature?