Are types propositions? (What are types exactly?)

Question

I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in programming languages and proof systems. However, I'm not entirely confident that my intuitive notion of what a type is, is correct.

My question is, is it valid to claim that types are propositions?

In other words the statement "n is a natural number" corresponds with the statement "n has the type 'natural number'" meaning that all the algebraic rules that involve natural numbers hold for n. (I.e. Said another way, algebraic rules are statements. Those statements that hold true for natural numbers also hold true for n.)

Then does this mean that a mathematical object can have more than one type?

Furthermore, I know that sets are not equivalent to types because you cannot have a set of all sets. Could I claim that if a set is a mathematical object similar to a number or a function, a type is a sort of meta-mathematical object and by the same logic a kind is a meta-meta-mathematical object? (in the sense that every "meta" indicates a higher level of abstraction...)

Does this have some kind of link to category theory?

Answer 1

The key role of types is to partition the objects of interest into different universes, rather than considering everything existing in one universe. Originally, types were devised to avoid paradoxes, but as you know, they have many other applications. Types give a way of classifying or stratifying objects (see blog entry).

Some work with the slogan that propositions are types, so your intuition certainly serves you well, though there is work such as Propositions as [Types] by Steve Awodey and Andrej Bauer that argues otherwise, namely that each type has an associated proposition. The distinction is made because types have computational content, whereas propositions don't.

An object can have more than one type due to subtyping and via type coercions.

Types are generally organised in a hierarchy, where kinds play the role of the type of types, but I wouldn't go as far as saying that types are meta-mathematical. Everything is going on at the same level – this is especially the case when dealing with dependent types.

There is a very strong link between types and category theory. Indeed, Bob Harper (quoting Lambek) says that Logics, Languages (where types reside), and Categories form a holy trinity. Quoting:

These three aspects give rise to three sects of worship: Logic, which gives primacy to proofs and propositions; Languages, which gives primacy to programs and types; Categories, which gives primacy to mappings and structures.

You should look at the Curry-Howard Correspondence to see the link between Logic and Programming Languages (types are propositions), and Cartesian Closed Categories, to see the between the relationship with Category Theory.