What are the practical issues with intersection and union types?

Question

I'm designing a simple statically typed functional programming language as a learning experience.

It appears that the type system I have implemented so far could (with a little extra work) incorporate intersection and union types, e.g. you could have:

• <Union String Integer>
• <Union Integer Foo>
• The intersection of the two types above would be a plain Integer
• The union of the two types would be <Union String Integer Foo>

The fact that this is possible, of course, doesn't necessary mean it is a good design idea. In particular, I'm a somewhat concerned about the implementation difficulties of keeping the types disjoint and/or handling overlaps.

What are the pros/cons of incorporating such features in the type system?

Answer 1

Here are a few things to keep in mind:

• Although we generally think we know what we mean by set-theoretic intersection and union, there have been several different takes on what exactly intersection and union types are. So, it's worth pinning this down before you embark on an implementation.
• One element which I think is awfully important for understanding intersections and unions is the concept of type refinement, essentially the idea that a program has a certain intrinsic "archetype" (e.g., "foo is a function from integers to integers"), which can then be refined to express more precise properties (e.g., "foo takes even integers to even integers and odd integers to odd integers"). With the concept of refinement in hand, the key property which distinguishes intersections and unions from products and sums is that the intersection/union of two types can be formed only if they refine the same archetype. In other words, the type formation rules for intersections and unions may be expressed like so (read "$S \sqsubset A$" as "$S$ refines $A$") $$\frac{S\sqsubset A \quad T \sqsubset A}{S\cap T\sqsubset A}\qquad \frac{S\sqsubset A \quad T \sqsubset A}{S\cup T\sqsubset A}$$ whereas the formation rules for ordinary products and sums are $$\frac{S\sqsubset A \quad T \sqsubset B}{S* T\sqsubset A*B}\qquad \frac{S\sqsubset A \quad T \sqsubset B}{S+T\sqsubset A+B}$$
• Since intersections and unions can be used to make more precise assertions about the run-time behavior of a program, it is natural that typing becomes sensitive to evaluation order. For example, papers (2) and (4) below explained why the "obvious" (and fairly standard) typing and subtyping rules for intersections and unions are actually unsound for ML-like languages (due to the presence of side effects and non-termination). You have been warned!
• For similar reasons, global type inference generally becomes impractical or undecidable. Indeed, the whole concept of "principal type" is arguably a red-herring, since a function may satisfy many different properties which are irrelevant to its intended use (e.g., "foo takes prime integers to integers greater than 7"). Instead, practical approaches to intersections and unions (see (3), (4)) are generally based on a combination of inference and checking.

I suppose some of the above points might sound negative, though I wouldn't call them "cons" but merely "realities" of intersection and union types. On the other hand, from a language design perspective, one reason for making the effort of supporting intersections and unions (and for getting them right!) is that they allow more precise properties of programs to be expressed in a fairly incremental way, requiring a much less drastic transformation than, say, dependent type theory.

A brief reading list:

1. Design of the Programming Language Forsythe by John C. Reynolds
2. Intersection Types and Computational Effects by Rowan Davies and Frank Pfenning
3. Practical Refinement-Type Checking by Rowan Davies (dissertation)
4. Tridirectional Typechecking by Joshua Dunfield and Frank Pfenning