|
By Dave, on December 9th, 2016
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
By Dave, on August 3rd, 2016
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
By Dave, on April 21st, 2013
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
By Dave, on March 2nd, 2012
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?
By Dave, on September 20th, 2011
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)
By Dave, on August 30th, 2011
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
By Dave, on August 29th, 2011
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
By Dave, on July 6th, 2011
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
By Dave, on March 7th, 2011
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
By Dave, on February 16th, 2011
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
|
|