#peter wegner

There is a universe V of all values, containing simple values like integers, data structures like pairs, records and variants, and functions. [...] A type is a set of elements of V. Not all subsets of V are legal types: they must obey some technical properties. The subsets of V obeying such properties are called ideals. All the types found in programming languages are ideals in this sense, so we don't have to worry too much about subsets of V which are not ideals. Hence, a type is an ideal, which is a set of values. Moreover, the set of all types (ideals) over V, when ordered by set inclusion, forms a lattice. The top of this lattice is the type Top (the set of all values, i.e. V itself). The bottom of the lattice is, essentially, the empty set (actually, it is the singleton set containing the least element of V). The phrase having a type is then interpreted as membership in the appropriate set. As ideals over V may overlap, a value can have many types. The set of types of any given programming language is generally only a small subset of the set of all ideals over V. For example any subset of the integers determines an ideal (and hence a type), and so does the set of all pairs with first element equal to 3. This generality is welcome, because it allows one to accommodate many different type systems in the same framework. One has to decide exactly which ideals are to be considered interesting in the context of a particular language. A particular type system is then a collection of ideals of V, which is usually identified by giving a language of type expressions and a mapping from type expressions to ideals. [...] A monomorphic type system is one in which each value belongs to at most one type (except for the least element of V which, by definition of ideal, belongs to all types). As types are sets, a value may belong to many types. A polymorphic type system is one in which large and interesting collections of values belong to many types. [...] Since types are sets, subtypes simply correspond to subsets. Moreover, the semantic assertion T1 is a subtype of T2 corresponds to the mathematical condition T1 ⊆ T2 in the type lattice. This gives a very simple interpretation for subrange types and inheritance [...] Let n..m denote the subtype of the type Int associated with the subrange n to m, extremes included, where n and m are known integers. The following type inclusion relations hold for integer subrange types: n..m ≤ n'..m' iff n' ≤ n and m ≤ m' where the ≤ on the left is type inclusion and those on the right are less or equal to. [...] Consider a function of type 3..7 → 7..9. This can also be considered a function of type 4..6 → 6..10, as it maps integers between 3 and 7 (and hence between 4 and 6) to integers between 7 and 9 (and hence between 6 and 10). Note that the domain shrinks while the codomain expands. In general we can formulate the inclusion rules for functions as follows: s→t ≤ s'→t' iff s' ≤ s and t ≤ t' note the (rather accidental) similarity of this rule and the rule for subranges, and how the inclusion on the domain is swapped. [...] The same line of reasoning applies to record types. [...] i.e., a record type A is a subtype of another record type B if A has all the attributes (fields) of B, and possibly more, and the types of the common attributes are respectively in the subtype relation. [...] Subtyping on record types corresponds to the concept of inheritance (subclasses) in languages, especially if records are allowed to have functional components. A class instance is a record with functions and local variables, and a subclass instance is a record with at least those functions and variables, and possibly more.

The usefulness of a type system lies not only in the set of types that can be represented but also in the kinds of relationships among types that can be expressed. The ability to express relations among types involves some ability to perform computations on types to determine whether they satisfy the desired relationship. Such computations could in principle be as powerful as computations performable on values.