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.