|
|||||
|
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 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 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 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? 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) 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 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 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 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 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 |
 |
||||
|
Copyright © 2020 David J. Pearce - All Rights Reserved 67 queries. 0.389 seconds. |
|||||
