Types are not sets.
You see, set theory has a number of features which simply don't apply to types, and vice-versa. For instance, an object has a single canonical type. It may be an instance of several different types, but only one of those types was used to instantiate it. Set theory has no notion of "canonical" sets.
Set theory allows you to create subsets on the fly, if you have a rule that describes what belongs to the subset. Type theory generally does not allow this. While most languages have a Number
type or something similar, they do not have an EvenNumber
type, nor would it be straightforward to create one. I mean, it's easy enough to define the type itself, but any existing Number
s which happen to be even will not be magically transformed into EvenNumber
Actually, saying that you can "create" subsets is somewhat disingenuous, because sets are a different kind of animal altogether. In set theory, those subsets already exist, in all the infinite ways you can define them. In type theory, we usually expect to be dealing with a finite (if large) number of types at any given time. The only types which are said to exist are those we've actually defined, not every type we could possibly define.
Sets are not allowed to directly or indirectly contain themselves. Some languages, such as Python, provide types with less regular structures (in Python, type
's canonical type is type
, and object
is considered an instance of object
). On the other hand, most languages do not allow user-defined types to engage in this sort of trickery.
Sets are commonly allowed to overlap without being contained in one another. This is uncommon in type theory, though some languages do support it in the form of multiple inheritance. Other languages, such as Java, only allow a restricted form of this or disallow it entirely.
The empty type exists (it's called the bottom type), but most languages do not support it, or do not regard it as a first-class type. The "type that contains all other types" also exists (it's called the top type) and is widely supported, unlike set theory.
NB: As some commenters previously pointed out (before the thread was moved to chat), it is possible to model types with set theory and other standard mathematical constructs. For instance, you could model type membership as a relation rather than modeling types as sets. But in practice, this is much simpler if you use category theory instead of set theory. This is how Haskell models its type theory, for example.
The notion of "subtyping" is really quite different from the notion of "subset." If X
is a subtype of Y
, it means we can substitute instances of Y
for instances of X
and the program will still "work" in some sense. This is behavioral rather than structural, though some languages (e.g. Go, Rust, arguably C) have chosen the latter for reasons of convenience, either to the programmer or the language implementation.