gotchaCritical
What exactly is the semantic difference between set and type?
Viewed 0 times
thewhattypedifferencebetweenandsemanticexactlyset
Problem
EDIT: I've now asked a similar question about the difference between categories and sets.
Every time I read about type theory (which admittedly is rather informal), I can't really understand how it differs from set theory, concretely.
I understand that there is a conceptual difference between saying "x belongs to a set X" and "x is of type X", because intuitively, a set is just a collection of objects, while a type has certain "properties". Nevertheless, sets are often defined according to properties as well, and if they are, then I am having trouble understanding how this distinction matters in any way.
So in the most concrete way possible, what exactly does it imply about $x$ to say that it is of type $T$, compared to saying that it is an element in the set $S$?
(You may pick any type and set that makes the comparison most clarifying).
Every time I read about type theory (which admittedly is rather informal), I can't really understand how it differs from set theory, concretely.
I understand that there is a conceptual difference between saying "x belongs to a set X" and "x is of type X", because intuitively, a set is just a collection of objects, while a type has certain "properties". Nevertheless, sets are often defined according to properties as well, and if they are, then I am having trouble understanding how this distinction matters in any way.
So in the most concrete way possible, what exactly does it imply about $x$ to say that it is of type $T$, compared to saying that it is an element in the set $S$?
(You may pick any type and set that makes the comparison most clarifying).
Solution
To understand the difference between sets and types, ones has to go back to pre-mathematical ideas of "collection" and "construction", and see how sets and types mathematize these.
There is a spectrum of possibilities on what mathematics is about. Two of these are:
-
We think of mathematics as an activity in which mathematical objects are constructed according to some rules (think of geometry as the activity of constructing points, lines and circles with a ruler and a compass).
Thus mathematical objects are organized according to how they are constructed, and there are different types of construction. A mathematical object is always constructed in some unique way, which determines its unique type.
-
We think of mathematics as a vast universe full of pre-existing mathematical objects (think of the geometric plane as given). We discover, analyze and think about these objects (we observe that there are points, lines and circles in the plane). We collect them into set. Usually we collect elements that have something in common (for instance, all lines passing through a given point), but in principle a set may hold together an arbitrary selection of objects. A set is specified by its elements, and only by its elements. A mathematical object may belong to many sets.
We are not saying that the above possibilities are the only two, or that any one of them completely describes what mathematics is. Nevertheless, each view can serve as a useful starting point for a general mathematical theory that usefully describes a wide range of mathematical activities.
It is natural to take a type $T$ and imagine the collection of all things that we can construct using the rules of $T$. This is the extension of $T$, and it is not $T$ itself. For instance, here are two types that have different rules of construction, but they have the same extension:
-
The type of pairs $(n, p)$ where $n$ is constructed as a natural number, and $p$ is constructed as a proof demonstrating that $n$ is an even prime number larger than $3$.
-
The type of pairs $(m, q)$ where $m$ is constructed as a natural number, and $q$ is constructed as a proof demonstrating that $m$ is an odd prime smaller than $2$.
Yes, these are silly trivial examples, but the point stands: both types have nothing in their extension, but they have different rules of construction. In contrast, the sets
$$\{ n \in \mathbb{N} \mid \text{$n$ is an even prime larger than $3$} \}$$
and
$$\{ m \in \mathbb{N} \mid \text{$m$ is an odd prime smaller than $2$} \}$$
are equal because they have the same elements.
Note that type theory is not about syntax. It is a mathematical theory of constructions, just like set theory is a mathematical theory of collections. It just so happens that the usual presentations of type theory emphasize syntax, and consequently people end up thinking type theory is syntax. This is not the case. To confuse a mathematical object (construction) with a syntactic expression that represents it (a term former) is a basic category mistake that has puzzled logicians for a long time, but not anymore.
There is a spectrum of possibilities on what mathematics is about. Two of these are:
-
We think of mathematics as an activity in which mathematical objects are constructed according to some rules (think of geometry as the activity of constructing points, lines and circles with a ruler and a compass).
Thus mathematical objects are organized according to how they are constructed, and there are different types of construction. A mathematical object is always constructed in some unique way, which determines its unique type.
-
We think of mathematics as a vast universe full of pre-existing mathematical objects (think of the geometric plane as given). We discover, analyze and think about these objects (we observe that there are points, lines and circles in the plane). We collect them into set. Usually we collect elements that have something in common (for instance, all lines passing through a given point), but in principle a set may hold together an arbitrary selection of objects. A set is specified by its elements, and only by its elements. A mathematical object may belong to many sets.
We are not saying that the above possibilities are the only two, or that any one of them completely describes what mathematics is. Nevertheless, each view can serve as a useful starting point for a general mathematical theory that usefully describes a wide range of mathematical activities.
It is natural to take a type $T$ and imagine the collection of all things that we can construct using the rules of $T$. This is the extension of $T$, and it is not $T$ itself. For instance, here are two types that have different rules of construction, but they have the same extension:
-
The type of pairs $(n, p)$ where $n$ is constructed as a natural number, and $p$ is constructed as a proof demonstrating that $n$ is an even prime number larger than $3$.
-
The type of pairs $(m, q)$ where $m$ is constructed as a natural number, and $q$ is constructed as a proof demonstrating that $m$ is an odd prime smaller than $2$.
Yes, these are silly trivial examples, but the point stands: both types have nothing in their extension, but they have different rules of construction. In contrast, the sets
$$\{ n \in \mathbb{N} \mid \text{$n$ is an even prime larger than $3$} \}$$
and
$$\{ m \in \mathbb{N} \mid \text{$m$ is an odd prime smaller than $2$} \}$$
are equal because they have the same elements.
Note that type theory is not about syntax. It is a mathematical theory of constructions, just like set theory is a mathematical theory of collections. It just so happens that the usual presentations of type theory emphasize syntax, and consequently people end up thinking type theory is syntax. This is not the case. To confuse a mathematical object (construction) with a syntactic expression that represents it (a term former) is a basic category mistake that has puzzled logicians for a long time, but not anymore.
Context
StackExchange Computer Science Q#91330, answer score: 59
Revisions (0)
No revisions yet.