<p>The main reason to prefer the colon notation <span class="math-container">$t : T$</span> to the membership relation <span class="math-container">$t \in T$</span> is that the membership relation can be misleading because <strong>types are not (just) collections</strong>.</p>

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

<p>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.</p>

<p>For instance a product type <span class="math-container">$A \times B$</span> 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 <span class="math-container">$A \times B$</span>. The definition of <span class="math-container">$A \times B$</span> does <em>not</em> start with the words "the collection of all ..." and neither does it say anywhere anything like "all elements of <span class="math-container">$A \times B$</span> are pairs" (but it <em>follows</em> from the definition that every element of <span class="math-container">$A \times B$</span> is <em>propositionally</em> equal to a pair). In constrast, the set-theoretic definition of <span class="math-container">$X \times Y$</span> <em>is</em> stated as "the set of all ordered pairs ...".</p>

<p>The notation <span class="math-container">$t : T$</span> signifies the fact that <span class="math-container">$t$</span> has the structure described by <span class="math-container">$T$</span>.</p>

<p>A type <span class="math-container">$T$</span> is not to be confused with its <strong>extension</strong>, which is the collection of all objects of type <span class="math-container">$T$</span>.  A type is <em>not</em> 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:</p>

<ol>
<li>The type of all even primes larger than two: <span class="math-container">$\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{iseven}(n) \times (n &gt; 2)$</span>. </li>
<li>The type of all odd primes smaller than two: <span class="math-container">$\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{isodd}(n) \times (n &lt; 2)$</span>.</li>
</ol>

<p>The extension of both is empty, but they are not the same type.</p>

<p>There are further differences between the type-theoretic <span class="math-container">$:$</span> and the set-theoretic <span class="math-container">$\in$</span>. An object <span class="math-container">$a$</span> 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 <span class="math-container">$t : T$</span> and <span class="math-container">$t : U$</span> then <span class="math-container">$T \equiv U$</span>. Or to put it differently, a type-theoretic construction <span class="math-container">$t$</span> has precisely one type <span class="math-container">$T$</span>, and in fact there is no way to have just an object <span class="math-container">$t$</span> without its (uniquely determined) type.</p>

<p>Another difference is that in set theory we can <em>deny</em> the fact that <span class="math-container">$a \in A$</span> by writing <span class="math-container">$\lnot (a \in A)$</span> or <span class="math-container">$a \not\in A$</span>. This is not possible in type theory, because <span class="math-container">$t : T$</span> is a <em>judgement</em> 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.</p>

CC BY-SA 4.0
2019-05-25T16:26:53.757Z
Andrej, great answer. Do you happen to know the historic origin of the colon notation?
Andreas Rossberg
CC BY-SA 4.0
2019-05-25T20:39:52.357Z
Alas, I do not. [Church's type theory](https://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf) used subscripts, i.e., $x_\alpha$ for a variable of type $\alpha$. Russell and Whitehead used $\epsilon$ for the relation of belonging to a class. Algol 68 puts types in front of variable names. The [1972 Martin-Löf type theory](http://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-1972.pdf) uses $\in$, and so does the [1984 version](http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-1984.pdf), but the [1994 version] uses a colon.
Andrej Bauer
CC BY-SA 4.0
2019-05-25T21:14:25.440Z
So your argument is that a type is a like a group? That makes sense, but the notation $g \in G$ is common in abstract algebra.
Gaslight Deceive Subvert
CC BY-SA 4.0
2019-05-26T07:22:14.520Z
@BjörnLindqvist: No, that is not my argument, that is *one remark* among several in my answer. Also, writing $g \in G$ is not problematic because the carrier of a group is a *set*, and by writing $g \in G$ we are not misleading anyone, we're just omitting an implicit coercion (from a group to its carrier). In type theory we would write $g : G$, and the proof assistant can insert the implicit coercion. A type is not just a set, and it is therefore customary and prudent to use a different notation, especially so that newcomers get to contemplate on the difference between a set and a type.
Andrej Bauer
CC BY-SA 4.0
2019-05-26T11:44:08.900Z
@BjörnLindqvist: I don't think this answer is the full story. Even in standard mathematics we use "$f : S→T$" to denote that $f$ is a function from $S$ to $T$. Why did we not use "$f ∈ (S→T)$" or something like that? Well, we just didn't. Of course, there is good reason to avoid the use of "$∈$" in a **presentation** of certain kinds of type theories, simply because we don't want ZFC-taught people to think it's like ZFC-sets, which obviously isn't the case. But that doesn't mean that the colon hasn't **already** been widely used long before type theory became popular.
user21820
CC BY-SA 4.0
2019-05-26T14:41:30.473Z
Of course the answer isn't the full story, I would think that much is obvious.
Andrej Bauer
CC BY-SA 4.0
2019-05-27T03:41:31.537Z
Could you elaborate on why those two types (of even primes greater than 2 and odd primes less than 2) are not "the same"? What do you even mean by that sameness? Surely you agree that we can show the types are isomorphic.
Mario Carneiro
CC BY-SA 4.0
2019-05-27T10:43:29.517Z
@MarioCarneiro: they are isomorphic, as you point out, but they are not judgmentally equal, i.e., if $x$ is a variable whose type is the first one, it does not have the type of the second one.
Andrej Bauer
CC BY-SA 4.0
2019-05-27T14:31:56.087Z
@user21820 "Why didn't we use $f\in (S\to T)$?" Just speculating: because mathematicians never thought of $S\to T$ as a set. For the history of this notation see [here](https://mathoverflow.net/questions/194377). I doubt that the colon from $f\colon S\to T$ was the inspiration for type theorists. More likely type theorists colon has to do with the fact that $\in$ is not a ASCII character.
Michael
CC BY-SA 4.0
2019-06-13T04:31:20.240Z
I don't have them with me but the answer might be in Kleene's or van Heijenoort's books.
Kaveh
CC BY-SA 4.0
2021-09-08T16:41:28.413Z
J. Zucker's "Forrnalization of Classical Mathematics in Automath" (1975) used a colon for typing relation. It seems that some currents of type theorists used colons, while others did not? Even the Automath community used "E" instead of colons in the early '70s, late '60s.
Alex Nelson
CC BY-SA 4.0
2019-05-25T13:43:29.883Z
2019-05-28T08:00:25.467Z
2019-05-28T08:00:25.467Z
Andrej Bauer
<p>Björn,</p>

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

<p><a href="https://i.sstatic.net/OKcBa.jpg" rel="noreferrer"><img src="https://i.sstatic.net/OKcBa.jpg" alt="First Google hit for Pascal"></a></p>

CC BY-SA 4.0
2019-05-25T14:05:37.423Z
Weren't there any earlier programming languages that used `:`?
Andrej Bauer
CC BY-SA 4.0
2019-05-25T15:54:16.960Z
@AndrejBauer indeed, I wrote "There's probably an earlier reference but..." to guard against that likely fact.
Bjørn Kjos-Hanssen
CC BY-SA 4.0
2019-05-25T20:24:08.757Z
@AndrejBauer Algol didn't. Was `:` used in theory papers before 1970s?
Gilles 'SO- stop being evil'
CC BY-SA 4.0
2019-05-27T13:29:31.303Z
Nice screenshot. I remember the arrival of Turbo Pascal 5.5. I never used Windows, though.
Carsten S
CC BY-SA 4.0
2019-05-27T14:33:22.740Z
Fortran has `REAL  ::  x` but I don't know if this came before Pascal.
Michael
CC BY-SA 4.0
2019-05-28T08:27:13.543Z
@Michael Fortran came earlier than Pascal (ca. 1955 vs. ca. 1970), but I think this specific syntax was introduced only in Fortran 90, so a lot later than Pascal. See e.g. here http://fortranwiki.org/fortran/show/Modernizing+Old+Fortran
Federico Poloni
CC BY-SA 4.0
2019-05-25T02:24:28.203Z
2019-05-25T02:24:28.203Z
Bjørn Kjos-Hanssen
<p>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.</p>

<p><a href="https://en.wikipedia.org/wiki/History_of_type_theory" rel="noreferrer">Type theory started out</a> in the early 20th century as an approach to the foundation of mathematics. <a href="https://en.wikipedia.org/wiki/Bertrand_Russell" rel="noreferrer">Bertrand Russel</a> discovered a <a href="https://en.wikipedia.org/wiki/Russell%27s_paradox" rel="noreferrer">paradox</a> 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.</p>

<p>In particular, many theories of types have a <em>syntactic</em> 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 <a href="https://en.wikipedia.org/wiki/Alonzo_Church" rel="noreferrer">Church</a>'s <a href="https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf" rel="noreferrer"><em>A Formulation of the Simple Theory of Types</em> (1940)</a></p>

<p>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 <a href="https://cstheory.stackexchange.com/a/43979">Andrej Bauer's answer here</a> and <a href="https://cs.stackexchange.com/questions/91330/what-exactly-is-the-semantic-difference-between-set-and-type">his answer on a related question</a> for some examples. That second thread has other answers worth reading.</p>

<p>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 <a href="https://en.wikipedia.org/wiki/Denotational_semantics" rel="noreferrer">denotational semantics</a> was a difficult problem in the early 1970s. The seminal paper here is <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.362.3367" rel="noreferrer"><em>Toward a mathematical semantics for computer languages</em> (1971)</a> by <a href="https://en.wikipedia.org/wiki/Dana_Scott" rel="noreferrer">Dana Scott</a> and <a href="https://en.wikipedia.org/wiki/Christopher_Strachey" rel="noreferrer">Christopher Strachey</a>. The <a href="https://en.wikibooks.org/wiki/Haskell/Denotational_semantics" rel="noreferrer">Haskell wikibook</a> has a good presentation of the topic.</p>

<p>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. <strong>Values have types, but so do other things, such as expressions and variables</strong>. For example, an expression in a typed programming language has a type even if it doesn't terminate. You might be willing to conflate <code>integer</code> and <span class="math-container">$\mathbb{Z}$</span>, but <code>(x := 0; while true; do x := x + 1; x)</code> is not an element of <span class="math-container">$\mathbb{Z}$</span>.</p>

<p>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 <a href="https://en.wikipedia.org/wiki/Pascal_(programming_language)" rel="noreferrer">Pascal</a> 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 <a href="https://hal.inria.fr/hal-01399694/document" rel="noreferrer"><em>Several Types of Types in Programming Languages</em></a>, 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.</p>

CC BY-SA 4.0
2019-05-25T20:23:23.790Z
2019-05-25T20:23:23.790Z
Gilles 'SO- stop being evil'
<p>Pierce (2002) introduces the <em>typing relation</em> on page 92 by writing:</p>

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

<p>and the footnote says The symbol <span class="math-container">$\in$</span> is often used instead of :. My question is simply <strong>why</strong> type theorists prefer to use : over <span class="math-container">$\in$</span>? If a type <span class="math-container">$T$</span> is a set of values then it makes perfect sense to write <span class="math-container">$t \in T$</span>, no new notation needed. </p>

<p>Is this similar to how some cs writers prefer <span class="math-container">$3n^2 = O(n^2)$</span> even thought it is abuse of notation and should be written <span class="math-container">$3n^2 \in O(n^2)$</span>?</p>

CC BY-SA 4.0
2019-05-25T03:59:03.813Z
The membership *predicate* $x \in X$ can be either true or false, whereas a typing *declaration* $x : X$ is generally interepreted as a factual statement that is *declared* to be true **or** it's truth can be derived by *purely* syntactic means. Contrast this to being a prime number, for which no syntactic method of membership suffices.
Musa Al-hassy
CC BY-SA 4.0
2019-05-25T13:09:13.913Z
@MusaAl-hassy Thank's for the explanation! Do you have a reference about it?
Gaslight Deceive Subvert
CC BY-SA 4.0
2019-05-25T13:25:44.723Z
@MusaAl-hassy: that's a misrepresentation of what is going on. It is not *declared* to be true, as that would mean that I can "declare" that "`false` : `int`", for example. Neither is it the case that the judgement must be necessarily derived by "purely syntactic means", for instance in the case of the internal type theory of a category with families.
Andrej Bauer
CC BY-SA 4.0
2019-05-25T17:28:23.440Z
Related question on cs.se: [What exactly is the semantic difference between set and type?](https://cs.stackexchange.com/questions/91330/)
Discrete lizard
CC BY-SA 4.0
2019-05-25T20:36:37.317Z
To add to @MusaAl-hassy's comment, in _computatioal type theory_ of Bob Constable, Stuart Allen, Bob Harper, et al., $\in$ is used routinely for typing judgments because it's more akin to a membership predicate (see [this](https://www.cs.cmu.edu/~rwh/talks/POPL18-Tutorial.pdf) talk, slide 25, for an example).
xrq
CC BY-SA 4.0
2019-05-26T07:24:15.493Z
@Discretelizard: Ah yes, this question felt like a deja vu to me.
Andrej Bauer
CC BY-SA 4.0
2019-05-26T10:14:02.110Z
Surely $3n^2\in O(n^2)$ is also an abuse of notation and should really be written $\lambda n.3n^2\in O(\lambda n.n^2)$? (Mathematicians might prefer $n\mapsto 3n^2\in O(n\mapsto n^2)$.)
Oscar Cunningham
<type-theory><notation>
Why colon to denote that a value belongs to a type?
Gaslight Deceive Subvert
# Why colon to denote that a value belongs to a type?

(Asked by: username_0 on 2019-05-24)

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)$?

**Tags:** type-theory, notation

> **Comments:**
> **username_1**: The membership *predicate* $x \in X$ can be either true or false, whereas a typing *declaration* $x : X$ is generally interepreted as a factual statement that is *declared* to be true **or** it's truth can be derived by *purely* syntactic means. Contrast this to being a prime number, for which no syntactic method of membership suffices.  
> **username_0**: @MusaAl-hassy Thank's for the explanation! Do you have a reference about it?  
> **username_2**: @MusaAl-hassy: that's a misrepresentation of what is going on. It is not *declared* to be true, as that would mean that I can "declare" that "`false` : `int`", for example. Neither is it the case that the judgement must be necessarily derived by "purely syntactic means", for instance in the case of the internal type theory of a category with families.  
> **username_3**: Related question on cs.se: [What exactly is the semantic difference between set and type?](https://cs.stackexchange.com/questions/91330/)  
> **username_4**: To add to @MusaAl-hassy's comment, in _computatioal type theory_ of Bob Constable, Stuart Allen, Bob Harper, et al., $\in$ is used routinely for typing judgments because it's more akin to a membership predicate (see [this](https://www.cs.cmu.edu/~rwh/talks/POPL18-Tutorial.pdf) talk, slide 25, for an example).  
> **username_2**: @Discretelizard: Ah yes, this question felt like a deja vu to me.  
> **username_5**: Surely $3n^2\in O(n^2)$ is also an abuse of notation and should really be written $\lambda n.3n^2\in O(\lambda n.n^2)$? (Mathematicians might prefer $n\mapsto 3n^2\in O(n\mapsto n^2)$.)  

---

## 3 answers

### Answer by username_13 on 2019-05-25. Score: 14 | Accepted answer

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](https://en.wikipedia.org/wiki/History_of_type_theory) in the early 20th century as an approach to the foundation of mathematics. [Bertrand Russel](https://en.wikipedia.org/wiki/Bertrand_Russell) discovered a [paradox](https://en.wikipedia.org/wiki/Russell%27s_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](https://en.wikipedia.org/wiki/Alonzo_Church)'s [*A Formulation of the Simple Theory of Types* (1940)](https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf)

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 [username_2's answer here](https://cstheory.stackexchange.com/a/43979) and [his answer on a related question](https://cs.stackexchange.com/questions/91330/what-exactly-is-the-semantic-difference-between-set-and-type) 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](https://en.wikipedia.org/wiki/Denotational_semantics) was a difficult problem in the early 1970s. The seminal paper here is [*Toward a mathematical semantics for computer languages* (1971)](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.362.3367) by [Dana Scott](https://en.wikipedia.org/wiki/Dana_Scott) and [Christopher Strachey](https://en.wikipedia.org/wiki/Christopher_Strachey). The [Haskell wikibook](https://en.wikibooks.org/wiki/Haskell/Denotational_semantics) 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](https://en.wikipedia.org/wiki/Pascal_(programming_language)) 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*](https://hal.inria.fr/hal-01399694/document), 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 by username_2 on 2019-05-25. Score: 39

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.

> **Comments:**
> **username_6**: Andrej, great answer. Do you happen to know the historic origin of the colon notation?  
> **username_2**: Alas, I do not. [Church's type theory](https://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf) used subscripts, i.e., $x_\alpha$ for a variable of type $\alpha$. Russell and Whitehead used $\epsilon$ for the relation of belonging to a class. Algol 68 puts types in front of variable names. The [1972 Martin-Löf type theory](http://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-1972.pdf) uses $\in$, and so does the [1984 version](http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-1984.pdf), but the [1994 version] uses a colon.  
> **username_0**: So your argument is that a type is a like a group? That makes sense, but the notation $g \in G$ is common in abstract algebra.  
> **username_2**: @BjörnLindqvist: No, that is not my argument, that is *one remark* among several in my answer. Also, writing $g \in G$ is not problematic because the carrier of a group is a *set*, and by writing $g \in G$ we are not misleading anyone, we're just omitting an implicit coercion (from a group to its carrier). In type theory we would write $g : G$, and the proof assistant can insert the implicit coercion. A type is not just a set, and it is therefore customary and prudent to use a different notation, especially so that newcomers get to contemplate on the difference between a set and a type.  
> **username_7**: @BjörnLindqvist: I don't think this answer is the full story. Even in standard mathematics we use "$f : S→T$" to denote that $f$ is a function from $S$ to $T$. Why did we not use "$f ∈ (S→T)$" or something like that? Well, we just didn't. Of course, there is good reason to avoid the use of "$∈$" in a **presentation** of certain kinds of type theories, simply because we don't want ZFC-taught people to think it's like ZFC-sets, which obviously isn't the case. But that doesn't mean that the colon hasn't **already** been widely used long before type theory became popular.  
> **username_2**: Of course the answer isn't the full story, I would think that much is obvious.  
> **username_8**: Could you elaborate on why those two types (of even primes greater than 2 and odd primes less than 2) are not "the same"? What do you even mean by that sameness? Surely you agree that we can show the types are isomorphic.  
> **username_2**: @MarioCarneiro: they are isomorphic, as you point out, but they are not judgmentally equal, i.e., if $x$ is a variable whose type is the first one, it does not have the type of the second one.  
> **username_9**: @username_7 "Why didn't we use $f\in (S\to T)$?" Just speculating: because mathematicians never thought of $S\to T$ as a set. For the history of this notation see [here](https://mathoverflow.net/questions/194377). I doubt that the colon from $f\colon S\to T$ was the inspiration for type theorists. More likely type theorists colon has to do with the fact that $\in$ is not a ASCII character.  
> **username_10**: I don't have them with me but the answer might be in Kleene's or van Heijenoort's books.  
> **username_11**: J. Zucker's "Forrnalization of Classical Mathematics in Automath" (1975) used a colon for typing relation. It seems that some currents of type theorists used colons, while others did not? Even the Automath community used "E" instead of colons in the early '70s, late '60s.  

---

### Answer by username_12 on 2019-05-25. Score: 5

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.sstatic.net/OKcBa.jpg)](https://i.sstatic.net/OKcBa.jpg)

> **Comments:**
> **username_2**: Weren't there any earlier programming languages that used `:`?  
> **username_12**: @AndrejBauer indeed, I wrote "There's probably an earlier reference but..." to guard against that likely fact.  
> **username_13**: @AndrejBauer Algol didn't. Was `:` used in theory papers before 1970s?  
> **username_14**: Nice screenshot. I remember the arrival of Turbo Pascal 5.5. I never used Windows, though.  
> **username_9**: Fortran has `REAL  ::  x` but I don't know if this came before Pascal.  
> **username_15**: @username_9 Fortran came earlier than Pascal (ca. 1955 vs. ca. 1970), but I think this specific syntax was introduced only in Fortran 90, so a lot later than Pascal. See e.g. here http://fortranwiki.org/fortran/show/Modernizing+Old+Fortran  

---

