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.


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

Implicit Coercions in Whiley

The issue of [[Type conversion|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 . . . → Read More: Implicit Coercions in Whiley

Compile-time Verification, It’s Not Just for Type Safety Any More

I just came across an interesting presentation over at InfoQ called “Compile-time Verification, It’s Not Just for Type Safety Any More“:

The talk is by Greg Young and focuses on .Net’s contracts library.  It’s quite interesting, and you can see the contracts in action.  From my perspective, what’s very interesting is that he shows . . . → Read More: Compile-time Verification, It’s Not Just for Type Safety Any More

Whiley v0.3.7 Released!

Development has continued at a fairly quick pace since the last release of Whiley.  However, with the impending start of term, things are bound to slow down.  Therefore, I’m making a release now a little sooner that otherwise planned.  This fixes a number of important bugs, finally allowing the compiler to compile my benchmark . . . → Read More: Whiley v0.3.7 Released!

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

Bits, Bytes and More Ambiguous Syntax

Recently, I added a first-class byte type to Whiley.  Unlike Java, this is not interpreted as some kind of signed or unsigned int. That’s because I find that very confusing since a byte is really just a sequence of bits without any interpretation.

Therefore, in Whiley, a byte is just that: a bit . . . → Read More: Bits, Bytes and More Ambiguous Syntax