On Data Types

A semantic model of types is proposed. This model interprets types as elements in an augmented domain constructed with the Smyth powerdomain constructor. In this domain types approximate the values of which they are types. Within this model, a type of an application f(x) is found by applying a type of f to a type of x. This becomes the basis of type checking and type inference. The model accomodates in a natural way type hierarchies, polymorphic functions, and recursive polymorphic types. A number of examples are worked out in some detail.