Why colon to denote that a value belongs to a type?

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 1

Because what's on the right of the colon isn't necessarily a set and what's on the left of the colon isn't necessarily a member of that set.

Type theory started out in the early 20th century as an approach to the foundation of mathematics. Bertrand Russel discovered a paradox in naive set theory, and he worked on type theory as a way to limit the expressive power of set theory to avoid this (and any other) paradox. Over the years, Russel and others have defined many theories of types. In some theories of types, types are sets with certain properties, but in others, they're a different kind of beast.

In particular, many theories of types have a syntactic formulation. There are rules that cause a thing to have a type. When the typing rules used as a foundation for a theory, it's important to distinguish what the typing rules say from what one might infer by applying additional external knowledge. This is especially important if the typing rules are a foundation for a proof theory: theorems that hold based on set theory with classical logic and the axiom of choice may or may not hold in a constructive logic, for example. One of the seminal papers in this domain is Church's A Formulation of the Simple Theory of Types (1940)

Perhaps the way in which the distinction between types and sets is the most apparent is that the most basic rule for sets, namely that two sets are equal iff they have the same elements, usually does not apply for types. See Andrej Bauer's answer here and his answer on a related question for some examples. That second thread has other answers worth reading.

In a typed calculus, to say that the types are sets is in fact to give a semantics to the types. Giving a calculus a type-theoretic semantics is not trivial. For example, suppose you're defining a language with functions. What set is a type of a function? Total functions are determined by their graph, as we're taught in set theory 101. But what about partial functions? Do you want to give all non-terminating functions the same semantics? You can't interpret types as sets for a calculus that allows recursive functions until you've answered that question. Giving programming languages or calculi a denotational semantics was a difficult problem in the early 1970s. The seminal paper here is Toward a mathematical semantics for computer languages (1971) by Dana Scott and Christopher Strachey. The Haskell wikibook has a good presentation of the topic.

As I wrote above, a second part of the answer is that even if you have managed to give types a set-theoretical semantics, the thing on the left of the colon isn't always an element of the set. Values have types, but so do other things, such as expressions and variables. For example, an expression in a typed programming language has a type even if it doesn't terminate. You might be willing to conflate integer and $\mathbb{Z}$, but (x := 0; while true; do x := x + 1; x) is not an element of $\mathbb{Z}$.

I don't know when the colon notation arose for types. It's now standard in semantics, and common in programming languages, but neither Russel nor Church used it. Algol didn't use it, but the heavily Algol-inspired language Pascal did in 1971. I suspect it wasn't the first, though, because many theory papers from the early 1970s use the notation, but I don't know of an earlier use. Interestingly, this was soon after the concepts of types from programming and from logic had been unified — as Simon Martini shows in Several Types of Types in Programming Languages, what was called a “type” in programming languages up to the 1960s came from the vernacular use of the word and not from type theory.

Answer 2

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.

Answer 3

Björn,

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