Computer Science Department
School of Computer Science, Carnegie Mellon University
A Unified System of Type Refinements
Types express properties of programs; typechecking is specification checking. However, the specifications expressed by types in conventional type systems are imprecise. Type refinements address this by allowing programmers to express more precise properties, while keeping typechecking decidable and practical.
We present a system of type refinements that unifies and extends past work on datasort and index refinements. We provide unified mechanisms of definite types, such as intersections, and indefinite types, such as unions. Through our development of contextual typing annotations, the tridirectional rule, and let-normal typechecking, we achieve a type system that is expressive and practical, requiring no user input besides type annotations. We show that our implementation of the type system can check several data structure invariants, as well as dimension types (an instance of invaluable refinements), in a subset of Standard ML.