An Imperative Type Hierarchy with Partial Products

Abstract

A type hierarchy for an imperative language defines an ordering on the types such that any application for small types may be reused for all larger types. The imperative facet makes this non-trivial; the straight-forward definitions will yield an inconsistent system. We introduce a new type constructor, the partial product, and show how to define a consistent hierarchy in the context of fully recursive types. A simple polymorphism is derived. By extending the types to include stuctural invariants we obtain a particularly appropriate notation for defining recursive types, that is superior to traditional type sums and products. We show how the ordering on types extends to an ordering on types with invariants. We allow the use of least upper bounds in type definitions and show how to resolve type equations involving these, and how to compute upper bounds of invariants.