Question: Pierce (2002) introduces the *typing relation* on page 92 by writing:

> 
> The typing relation for arithmetic expressions, written "t : T", is defined by
>  a set of inference rules assigning types to terms
> 
> 
> 

and the footnote says The symbol $\in$ is often used instead of :. My question is simply **why** type theorists prefer to use : over $\in$? If a type $T$ is a set of values then it makes perfect sense to write $t \in T$, no new notation needed. 

Is this similar to how some cs writers prefer $3n^2 = O(n^2)$ even thought it is abuse of notation and should be written $3n^2 \in O(n^2)$?

Answer: 
The main reason to prefer the colon notation $t : T$ to the membership relation $t \in T$ is that the membership relation can be misleading because **types are not (just) collections**.

[**Supplemental:** I should note that historically type theory *was* written using $\in$. Martin-Löf's conception of type was meant to capture sets constructively, and already Russell and Whitehead used $\epsilon$ for the class memebrship. It would be interesting to track down the moment when $:$ became more prevalent than $\in$.]

A type describes a certain kind of construction, i.e., how to make objects with a certain structure, how to use them, and what equations holds about them.

For instance a product type $A \times B$ has introduction rules that explain how to make ordered pairs, and elimination rules explaining that we can project the first and the second components from any element of $A \times B$. The definition of $A \times B$ does *not* start with the words "the collection of all ..." and neither does it say anywhere anything like "all elements of $A \times B$ are pairs" (but it *follows* from the definition that every element of $A \times B$ is *propositionally* equal to a pair). In constrast, the set-theoretic definition of $X \times Y$ *is* stated as "the set of all ordered pairs ...".

The notation $t : T$ signifies the fact that $t$ has the structure described by $T$.

A type $T$ is not to be confused with its **extension**, which is the collection of all objects of type $T$. A type is *not* determined by its extension, just like a group is not determined by its carrier set. Furthermore, it may happen that two types have the same extension, but are different, for instance:

1. The type of all even primes larger than two: $\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{iseven}(n) \times (n > 2)$.
2. The type of all odd primes smaller than two: $\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{isodd}(n) \times (n < 2)$.

The extension of both is empty, but they are not the same type.

There are further differences between the type-theoretic $:$ and the set-theoretic $\in$. An object $a$ in set theory exists independently of what sets it belongs to, and it may belong to several sets. In contrast, most type theories satisfy uniqueness of typing: if $t : T$ and $t : U$ then $T \equiv U$. Or to put it differently, a type-theoretic construction $t$ has precisely one type $T$, and in fact there is no way to have just an object $t$ without its (uniquely determined) type.

Another difference is that in set theory we can *deny* the fact that $a \in A$ by writing $\lnot (a \in A)$ or $a \not\in A$. This is not possible in type theory, because $t : T$ is a *judgement* which can be derived using the rules of type theory, but there is nothing in type theory that would allow us to state that something has not been derived. When a child makes something from LEGO blocks they proudly run to their parents to show them the construction, but they never run to their parents to show them what they didn't make.
Björn,

There's probably an earlier reference but for one thing, the colon was used in the Pascal programming language: 

[![First Google hit for Pascal](https://i.stack.imgur.com/OKcBa.jpg)](https://i.stack.imgur.com/OKcBa.jpg)