Abstract
We present Stardust, an implementation of a type system for a subset of ML with type
refinements, intersection types, and union types, enabling programmers to legibly
specify certain classes of program invariants that are verified at compile time.
This is the first implementation of unrestricted intersection and union types in a
mainstream functional programming setting, as well as the first implementation
of a system with both datasort and index refinements. The
system—with the assistance of external constraint solvers—supports integer,
Boolean and dimensional index refinements; we apply both
value refinements (to check red-black tree invariants) and invaluable
refinements (to check dimensional consistency). While typechecking with intersection
and union types is intrinsically complex, our experience so far suggests that it can be
practical in many instances.
|