Flow Typing with Constrained Types

Wednesday, 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). In doing so, I came across an interesting problem which I wanted to get down on paper. The problem arises when flow typing meets constrained types (a.k.a. types with invariants). What does a constrained type look like? Here’s an example in Whiley:

type nat is (int x) where x >= 0

This defines a type nat which contain all integer values x, where x >= 0. Constrained types are quite powerful and Whiley attempts to seamlessly integrate them with flow typing. Here’s a simple program to illustrate:

function abs(int x) -> (nat r):
    if x >= 0:
        return x
    else:
        return -x

The type of x is initially int. On the true branch, we know x >= 0 and (roughly speaking) the compiler automatically promotes x to type nat as needed.

The Problem

An interesting challenge arises within the compiler when reasoning about constrained types and flow typing. To understand, we need to consider how flow typing works in general. The following gives a rough outline:

S x = ...

if x is T:
   ...
else:
   ...

Here, S and T are some arbitrary types where T is a subtype of S. The compiler retypes variable x on the true branch to have type S & T and, on the false branch, to type S & !T (which you can think of as S - T). To make it concrete, consider the case for int|null and int:

int|null x = ...

if x is int:
   ...
else:
   ...

On the true branch, x has type (int|null)&int (which reduces to int) and, on the false branch, it has type (int|null)&!int (which reduces to null).

The basic plan outlined above works pretty well, but things get interesting with constrained types. For example, let’s use nat for the type test instead of int above:

int|null x = ...

if x is nat:
   ...
else:
   ...

The type of x on the true branch is (int|null)&nat, but what does this reduce to? A simple idea is to replace nat with its underlying type (i.e. int). We know this works as it’s exactly what we had before. But, what about the false branch? Reducing (int|null)&!nat in this way gives us null as before which, unfortunately, is wrong. The problem is that, on the false branch, x can still hold values of int type (i.e. negative values).

Mitigating Factors

The Whiley compiler already reasons correctly about flow typing in the presence of arbitrary conditionals. For example, consider this variant on our example from before:

int|null x = ...

if x is int && x >= 0:
   ...
else:
   ...

In this case, the Whiley compiler will correctly conclude that x has type int|null on the false branch. Then why not just expand constrained types like this and be done? That’s a good question. The answer is that, if we expand types in this way, we lose nominal information about them. For example, we’d lose the connection between x and type nat above, as x’s type on the either branch would be in terms of int and null only.

So, do we really need this nominal information? The answer is, technically speaking, no we don’t. Expanding types in this way is how the Whiley compiler currently works. But, nominal information helps with providing good error messages and, turns out, that’s important!

The Solution?

My proposed solution stems from ideas currently being used in the Whiley compiler, namely the concept of maximal and minimal consumption of types. The idea is that the maximal consumption of a type is the largest set of values it could consume. For type nat, the maximal consumption is int. The minimal consumption is the exact oppostite — the smallest set of values it must consume. For type nat, this is void because nat does not consume all possible integers. Note that the minimal consumption is not always void. For example, the minimal consumption for null|nat is null because null values are always consumed.

This probably seems a little confusing right now, but it will start to make sense! The key idea behind my solution is the introduction of two new operators over types, namely ⌈T⌉ (ceiling) and ⌊T⌋ (floor) for representing maximal and minimal consumption for a type T. With these, we can now correctly type our program from before without losing nominal information:

int|null x = ...

if x is nat:
   ...
else:
   ...

The point of these new operators is that they allow us to delay calculating the underlying type for x until we need it. In other words, they allow us to retain nominal information for as long as possible.

Observations

These two operators are interesting and it turns out there are few observations we can make about them:

For any primitive type T, we have that T is equivalent to both ⌊T⌋ and ⌈T⌉.
For any negation type !T, we have that ⌊!T⌋ is equivalent to !⌈T⌉ and ⌈!T⌉ is equivalent to !⌊T⌋.
For any union type T1 || T2, we have that ⌊T1 || T2⌋ is equivalent to ⌊T1⌋ || ⌊T2⌋, whilst ⌈T1 || T2⌉ is equivalent to ⌈T1⌉ || ⌈T2⌉.
For any intersection type T1 && T2, we have that ⌊T1 && T2⌋ is equivalent to ⌊T1⌋ && ⌊T2⌋, whilst ⌈T1 && T2⌉ is equivalent to ⌈T1⌉ || ⌈T2⌉.
For any nominal type N declared as T where e, we have that ⌊N⌋ is equivalent to void and ⌈T⌉ is equivalent to T.

Conclusion

Using these two new operators provides a simple way to reason about flow typing over constrained types. The next job for me is to implement this within the Whiley compiler!

References

Here’s an interesting paper on constrained types:

Constrained types for object-oriented languages, Nathaniel Nystrom, Vijay Saraswat, Jens Palsberg, Christian Grothoff. In Proceedings of OOPSLA, 2008. (LINK)