<p>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 <a href="http://scienceblogs.com/goodmath/2007/11/tiptoeing_into_type_theory.php">blog entry</a>).</p>

<p>Some work with the slogan that <em>propositions are types</em>, so your intuition certainly serves you well, though there is work such as <a href="http://andrej.com/papers/brackets_a4.pdf">Propositions as [Types]</a> 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. </p>

<p>An object can have more than one type due to <strong>subtyping</strong> and via <strong>type coercions</strong>.</p>

<p>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 <a href="http://en.wikipedia.org/wiki/Dependent_type">dependent types</a>.</p>

<p>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 <a href="http://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/">holy trinity</a>. Quoting:</p>

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

<p>You should look at the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard Correspondence</a> to see the link between Logic and Programming Languages (types are propositions), and <a href="http://en.wikipedia.org/wiki/Cartesian_closed_category">Cartesian Closed Categories</a>, to see the between the relationship with Category Theory.</p>

CC BY-SA 2.5
2011-04-04T14:56:48.837Z
Thank you the first link was especially helpful! In it Mark informs that there exists a "total relation <" over types. So does this mean that all "propositions" of a type must also include all "propositions" in the types below them? I expected that it would at least be a "partial relation <" over types....
Rehno Lindeque
CC BY-SA 2.5
2011-04-04T17:07:49.367Z
As I read it there is a total order over atoms, which was in place merely to ensure that there is an infinite number of atoms.
Dave Clarke
CC BY-SA 2.5
2011-04-04T22:47:24.290Z
Oh I see I got confused between the "Axiom of Comprehension" and the "Axiom of infinity"... Would a type 'nat' (the type of all natural numbers) be an "infinite level 0 type"?
Rehno Lindeque
CC BY-SA 2.5
2011-04-05T08:24:07.107Z
The "holy trinity" is really due to Lambek.  Cf. the discussion of type theory in Lambek&Scott (1986).  I've heard that in McGill one talks of the Curry-Howard-Lambek correspondence.
Charles Stewart
CC BY-SA 2.5
2011-04-05T15:31:27.023Z
@Charles:  I agree that Lambek is under-credited for his massive contribution, even if, ironically, it was reading the Lambek and Scott book that convinced me that the "holy trinity" is bogus:  it breaks down in the presence of potential non-termination.
Marc Hamann
CC BY-SA 2.5
2011-04-03T18:27:25.690Z
2011-04-05T12:13:48.220Z
2011-04-05T12:13:48.220Z
Dave Clarke
<p>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.</p>

<p>My question is, is it valid to claim that types are propositions? </p>

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

<p>Then does this mean that a mathematical object can have more than one type?</p>

<p>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 <em>set</em> is a mathematical object similar to a <em>number</em> or a <em>function</em>, a <em>type</em> is a sort of meta-mathematical object and by the same logic a <em>kind</em> is a meta-meta-mathematical object? (in the sense that every "meta" indicates a higher level of abstraction...)</p>

<p>Does this have some kind of link to category theory?</p>

CC BY-SA 2.5
2011-04-03T16:50:34.563Z
A closely related question: [Proofs/Programs and Propositions/Types](http://cstheory.stackexchange.com/questions/5235/what-is-the-difference-between-proofs-and-programs-or-between-propositions-and-t)
Marc Hamann
CC BY-SA 2.5
2011-04-03T17:17:06.367Z
Another related discussion: [Classification of Lambda Calculi](http://cstheory.stackexchange.com/questions/5834/classification-of-typed-untyped-lambda-calculi)
Marc Hamann
CC BY-SA 2.5
2011-04-04T16:35:07.557Z
Found another nice article here http://scientopia.org/blogs/goodmath/2009/11/17/types-in-haskell-types-are-propositions-programs-are-proofs/
Rehno Lindeque
CC BY-SA 2.5
2011-04-04T21:30:43.423Z
In some sense this boils down to a question of ontology. What is a set, a proposition etc. Further there are lots of people that think of types as sets aswell. If one wants to be more precise one can distinguish between small types (which are sets) and universe types. For a nice read that concerns some of this stuff I recommend Martin-Löfs classic paper "Intuitionistic Type Theory"
Tobias Raski
CC BY-SA 3.0
2011-04-09T22:01:39.687Z
Someone should write an answer from a Homotopy Type Theory point of view.
Robin Green
<lo.logic><type-theory><proof-theory>
Are types propositions? (What are types exactly?)
Rehno Lindeque
# Are types propositions? (What are types exactly?)

(Asked by: username_0 on 2011-04-03)

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?

**Tags:** lo.logic, type-theory, proof-theory
> **Comments:**
> **username_1**: A closely related question: [Proofs/Programs and Propositions/Types](http://cstheory.stackexchange.com/questions/5235/what-is-the-difference-between-proofs-and-programs-or-between-propositions-and-t)  
> **username_1**: Another related discussion: [Classification of Lambda Calculi](http://cstheory.stackexchange.com/questions/5834/classification-of-typed-untyped-lambda-calculi)  
> **username_0**: Found another nice article here http://scientopia.org/blogs/goodmath/2009/11/17/types-in-haskell-types-are-propositions-programs-are-proofs/  
> **username_2**: In some sense this boils down to a question of ontology. What is a set, a proposition etc. Further there are lots of people that think of types as sets aswell. If one wants to be more precise one can distinguish between small types (which are sets) and universe types. For a nice read that concerns some of this stuff I recommend Martin-Löfs classic paper "Intuitionistic Type Theory"  
> **username_3**: Someone should write an answer from a Homotopy Type Theory point of view.  

---

## 1 answers

### Answer by username_4 on 2011-04-03. Score: 20 | Accepted answer

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](http://scienceblogs.com/goodmath/2007/11/tiptoeing_into_type_theory.php)).

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]](http://andrej.com/papers/brackets_a4.pdf) 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](http://en.wikipedia.org/wiki/Dependent_type).

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](http://existentialtype.wordpress.com/2011/03/27/the-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](http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) to see the link between Logic and Programming Languages (types are propositions), and [Cartesian Closed Categories](http://en.wikipedia.org/wiki/Cartesian_closed_category), to see the between the relationship with Category Theory.

> **Comments:**
> **username_0**: Thank you the first link was especially helpful! In it Mark informs that there exists a "total relation <" over types. So does this mean that all "propositions" of a type must also include all "propositions" in the types below them? I expected that it would at least be a "partial relation <" over types....  
> **username_4**: As I read it there is a total order over atoms, which was in place merely to ensure that there is an infinite number of atoms.  
> **username_0**: Oh I see I got confused between the "Axiom of Comprehension" and the "Axiom of infinity"... Would a type 'nat' (the type of all natural numbers) be an "infinite level 0 type"?  
> **username_5**: The "holy trinity" is really due to Lambek.  Cf. the discussion of type theory in Lambek&Scott (1986).  I've heard that in McGill one talks of the Curry-Howard-Lambek correspondence.  
> **username_1**: @Charles:  I agree that Lambek is under-credited for his massive contribution, even if, ironically, it was reading the Lambek and Scott book that convinced me that the "holy trinity" is bogus:  it breaks down in the presence of potential non-termination.  

---

