Articles

Formalising Flow Typing with Union, Intersection and Negation Types

The Whiley language takes an unusual approaching to static typing called flow typing.  This helps to give Whiley the look-and-feel of a dynamically typed language.  The key idea behind flow typing is to allow variables to have different types at different points in a program.  For example, consider the following code written in a typical object oriented language (i.e. Java):

public class Square {
  private int x, y, len;

  ...

  public boolean equals(Object o) {
    if(o instanceof Square) {
      Square s = (Square) o;
      return x == s.x &&
             y == s.y &&
             len == s.len;
    }
    return false;
} }

What is frustrating here, is that we need to cast variable o to an entirely new variable s. The condition o instanceof Square asserts that variable o has type Square — and, the compiler should really be able to exploit this to avoid the unnecessary cast.

In Whiley, the compiler is able (amongst other things) to exploit type tests in this manner. For example, consider the following Whiley program:

define Square as { int x, int y, int len }
define Circle as { int x, int y, int radius }
define Shape as Square | Circle

boolean equals(Square s1, Shape s2):
   if s2 is Square:
      return s1.x == s2.x &&
             s1.y == s2.y &&
             s1.len == s2.len
   else:
      return false

In this example, no casting is necessary for variable s2 as the Whiley compiler knows it has type Square when the condition s2 is Square holds. An interesting question is: what type does s2 have on the false branch? Well, clearly, it is not a Square. And, that’s exactly how it’s implemented in the compiler — using a negation type. A negation type ¬T represents a type containing everything except T. In our example above, the type of s2 on the false branch is Shape & ¬Square. Here, T1 & T2 represents the intersection of two types T1 and T2. Thus, Shape & ¬Square represents everything in Shape but not in Square.

Subtyping Semantics

In building a compiler, it’s obviously important to develop algorithms for manipulating the types being used.  In this article, I want to focus on the algorithm for subtyping.  This simply reports whether or not a type T1 subtypes a type T2, denoted T1 <= T2. Based on the description given so far, one has an intuitive understanding of types as sets. That is, a type T represents the set of values which can be held in a variable declared with type T. In this way, we can think of T1 being a subtype of T2 if the set of values represented by T1 is a subset of those represented by T2.

We now begin to formalise more precisely what types in Whiley mean (i.e. their semantics). We use the following language of types, which is a cut-down version of those found in Whiley:

Here, any is the type containing all values, int is the type of integers, (T1,...,Tn) is a tuple type, ¬T is a negation type, T1 /\ T2 an intersection type (written T1 & T2 in Whiley source syntax), and T1 \/ T2 a union type (written T1 | T2 in Whiley source syntax).

To accompany our language of types, we need to define what constitutes a value in the system:

Here, v represents a value which is one of two possibilities: either it is an integer, or it is a tuple value the form (v1,...,vn).  Using this we can give a semantic interpretation of types in our language:

Here, we have defined a way to construct the set of values represented by a given type  T.  Whilst this may all seem rather mundane, it provides the necessary foundation for the subtyping algorithm.

An (Incomplete) Subtyping Algorithm

The subtyping algorithm is intended to determine when a type T1 is a subtype of a type T2.  Or, equivalently, when the set of values represented by T1 is a subset of those represented by T2. The algorithm is surprisingly difficult to get right, and it has taken me sometime to develop. The following represents a good attempt to capture the algorithm and is presented as a series of recursive “type rules” covering the different possible forms of T1 and T2:

Under these rules, we can for example show that (int,int) is a subtype of (any,any) and, likewise, that (int,int)is a subtype of (int,any)|(any,int).

The real challenge with the above subtyping rules is: how do I know they are right? Obviously, I want to be sure that the type checking algorithm in my compiler will work as expected.  But, it’s rather difficult to decide this just by staring at the rules.  We need to break the problem down and we do this using the following notions of soundness and completeness:

  • Soundness.  If the algorithm decides T1 subtypes T2, then it must follow that every value in T1 is also in T2.
  • Completeness.  If every value in T1 is also in T2, then the algorithm must decide that T1 subtypes T2.

In fact, the above rules can be shown as sound.  However, they are not complete.  For example, we cannot show that any is a subtype of int | ¬int — a fact which is indeed true under our semantic interpretation.

Fixing the Subtyping Algorithm

Now, the question is:

Is there a sound and complete algorithm for subtyping testing in this language and, if so, what is it?

The first part of the question (i.e. existence) was already shown by Frisch, Castagna, and Benzaken in their excellent (albeit complicated) paper.

The second part of the question (i.e. finding an actual algorithm) is also very important for me since I’m implementing an actual compiler.  To figure this out, I went back to the drawing board several times and, finally, found a reasonable algorithm which is discussed here:

  • Sound and Complete Flow Typing with Unions, Intersections and Negations. David J. Pearce. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013 (to appear) [PDF]

I won’t go into all the details here since its quite involved and the paper does a good job explaining things.  However, the key idea is to represent types in a “special form” such that we can easily perform the subtype tests.  The challenge is then to convert any given type T into its corresponding “special form”…

That’s all for now!

2 comments to Formalising Flow Typing with Union, Intersection and Negation Types

  • This is cool and the logic is very pretty. Negation types are obviously integral to the formal type system. Do they have a more practical use in the language? I noticed you did not provide a Whiley language representation of “¬T” ! So, I wonder if there are any benefits to implementing one. Constructions similar to your first example could simply test for memberhip of a negation type by transposing the two branches of the if-statement:

    if s2 is (not T):
    foo(…)
    else:
    bar(…)

    Becomes:

    if s2 is T:
    bar(…)
    else:
    foo(…)

    In terms of syntactic requirements, I’m unsure if there is code that *requires* a variable to be of type (not T) — for instance if the else branch of your example had simply had s2 of type any, nothing would be apparently broken in the program: the code in that branch does not demand a (not T) variable. Is there possible code that could?

  • Hi Edmund,

    Yeah, so there is a Whiley source syntax for negation types: !T

    But, the more general question you raise is whether or not these are useful to the programmer (i.e. other than as a hidden feature of the subtype algorithm). That’s a good question. I suppose one could imagine a situation where we have a function f() which wants to accept a parameter which can be anything *except* an int. In such case, its type would be f(!int). But, it is still unclear to me whether this is really useful or not …

Leave a Reply

 

 

 

You can use these HTML tags

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>