# What is semantics of "type"? Do "types" of "type theory" semantically differ from "set" of set theory?

"To be of a (certain type)" is a fundamental relationship for ontology and the computer science "ontologies" are in the core of Semantic Web (which is my interest). But I did not encounter a mathematical treatment of types. The "type theory" of New Foundations looks to me like "yet another set theory", because I do not see anything in its axioms which would hint to a treatment of types as different from collections. Can anybody please elaborate on this?

• @YemonChoi: thanks, fixed! Jun 30, 2014 at 13:49
• See Type Theory for history and motivation and see Church's Type Theory for a formal treatment. Jun 30, 2014 at 16:15

Yes, there is a rich field of mathematical treatments of types, in the sense of programming languages. However, New Foundations and Russell’s earlier theories of types are very atypical of what is now generally known as Type Theory.

A good place to start is with something like the typed λ-calculi of Church and others. These may exactly be seen as minimal programming languages, and serious modern functional programming languages like Haskell and OCaml (and relatives) are based very closely on more elaborate versions of these, with lots of syntactic sugar and clever type extensions added.

On the other hand, one may elaborate on these type systems in different directions to analyse how datatypes work in more pragmatically designed languages (C, Java, etc.).

In all of these, though, the difference from set theory is not so much in what types themselves are seen as — in most type systems I know, they are still viewed essentially as just abstract collections. There are two main differences with set theory:

1. the operations provided for constructing types and elements of types are typically very concrete and constructive, and mirror familiar constructs available in programming languages.

For instance, a type theory may well have a basic construct which, for a type A, provides a type List A, of lists of elements of A.

2. in (most) set theories, sets are collections from an ambient universe of sets; everything is a set, any set may be an element of any other set, and “being-an-element-of” is a relation, a property with a truth-value. In most type theories, types are not subcollections of some ambient collection — they are independent collections of elements.

So in set theory, a statement “for every prime number $$p$$, …” officially means “for every $$p$$, if $$p$$ is a number, and $$p$$ is prime, then…” — so the quantifier allows e.g. $$\mathbb{R}$$ as a valid value for $$p$$! In type theory, it would formally become “for every number $$p$$, if $$p$$ is prime then …” — primeness may be a property, but being a number is the basic type of thing p is declared to be as soon as it was considered. Every object you ever talk about has some type. You can’t (within the language of the theory) take the number 100, and then ask “is 100 a string?” — being of a type isn’t a property, it’s a declaration that’s made when a variable is introduced, or that’s deduced for a derived term like (n+5). In practical programming terms, this roughly says that the implementations of objects are well-sealed abstractions: an implementation may use the same underlying representation for some integer and some string, but the language can only access them as an integer and as a string. (Of course, type systems that are specifically designed to closely model existing languages may throw out such abstractions.)

There are lots of good introductions to type theory out there. The Wikipedia page gives a good start; for a serious book on type theory from a programming languages point of view, that’ll take you as far as you need to go, I recommend Bob Harper’s Practical foundations of programming languages, available as a pdf from his webpage. He’s highly opinionated and his more polemical statements must be taken with a large grain of salt, but he’s a fantastic writer, with a beautiful viewpoint on the field.