|
|||||
|
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 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! 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 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 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 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 Introduction Over the last few months, I’ve been working on the type system underpinning Whiley. A key feature is the use of 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 and turn . . . → 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 One problem causing me a headache is how to implement structural subtyping for 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 a fairly straightforward definition . . . → Read More: A Problem with Structural Subtyping and Recusive Types |
 |
||||
|
Copyright © 2012 David J. Pearce - All Rights Reserved 62 queries. 0.813 seconds. |
|||||
Popular Posts