Next: Relationship to Programming Up: Introduction to Type Previous: Semantics

# Relationship to Set Theory

Type theory is similar to set  theory in many ways, and one who is unfamiliar with the subject may not see readily how to distinguish the two. This section is intended to help. A type is like a set in these respects: it has elements, there are subtypes, and we can form products, unions and function spaces of types. A type is unlike a set in many ways too; for instance, two sets are considered equal exactly when they have the same elements, whereas in types are equal  only when they have the same structure. For example, void and `{x:int|x<x}` are both types with no members, but they are not equal.

The major differences between type theory and set theory emerge at a global level. That is, one cannot say much about the difference between the type int of integers and the set Z of integers, but one can notice that in type theory the concept of equality is given with each type, so we write x=y in int and x=y in int#atom. In set theory, on the other hand, equality is an absolute concept defined once for all sets. Moreover, set theory can be organized so that all objects of the theory are sets, while type theory requires certain primitive elements, such as individual integers, pairs, and functions, which are not types. Another major global difference between the theories concerns the method for building large types and large sets. In set theory one can use the union and power set axioms to build progressively larger sets. In fact, given any indexed family of sets, , the union of these sets exists. In type theory there are no union and power type operators. Given a family of types S(x) indexed by A, they can be put together into a disjoint union, x:A#S(x), or into a product, x:A->S(x), but there is no way to collect only the members of the S(x). Large unstructured collections of types can be obtained only from the universes,  U1, U2,... .

Another global difference between the two theories is that set theory typically allows so--called impredicative  set formation in that a set can be defined in terms of a collection which contains the set being defined. For instance, the subgroup H of a group G generated by elements is often defined to be the least among all subgroups of G containing the . However, this definition requires quantifying over a collection containing the set being defined. The type theory presented here depends on no such impredicative concepts.

For set theories, such as Myhill's CST [Myhill 75],  which do not employ impredicative concepts, Peter Aczel [Aczel 77,Aczel 78] has shown a method of defining such theories in a type theory similar to .

Both type theory and set theory can play the role of a foundational  theory. That is, the concepts used in these theories are fundamental. They can be taken as irreducible primitive ideas which are explained by a mixture of intuition and appeal to defining rules. The view of the world one gets from inside each theory is quite distinct. It seems to us that the view from type theory places more of the concepts of computer science in sharp focus and proper context than does the view from set theory.

Next: Relationship to Programming Up: Introduction to Type Previous: Semantics

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995