Types as Intervals

To accommodate polymorphic data types and operations, several computer scientists-most notably MacQueen, Plotkin, and Sethi-have proposed form&zing types as ideals. Although this approach is intuitively appealing, the resulting type system is both complex and restrictive because the type constructor that creates function types is not monotonic, and hence not computable. As a result, types cannot be treated as data values, precluding the for-malization of type constructors and polymorphic program modules (where types are values) as higher order computable functions. Moreover, recursive definitions of new types do not necessarily have solutions. This paper proposes a new formulation of types-called interuo&that subsumes the theory of types as ideals, yet avoids the pathologies caused by non-monotonic type constructors. In particular, the set of interval types contains the set of ideal types as a proper subset and all of the primitive type operations on intervals are extensions of the corresponding operations on ideals. Nevertheless, all of the primitive interval type constructors includ-ing the function type constructor and type quantifiers are comput-able operations. Consequently, types are higher order data values that can be freely manipulated within programs. The key idea underlying the formalization of types as intervals is that negafive information should be included in the description of a type. Negative information identifies the finite elements that do not belong to a type, just as conventional, positive information identifies the elements that do. Unless the negative information in a type description is the exact complement of the positive informa-tion, the description is partial in the sense that it approximates many different types-an interval of ideals between the positive information and the complement of the negative information. Although programmers typically deal with total (maximal) types, partial types appear to be an essential feature of a comprehensive polymorphic type system that accommodates types as data, just as partial functions are essential in any universal programming language. 1