25
$\begingroup$

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?

$\endgroup$
  • 5
    $\begingroup$ A closely related question: Proofs/Programs and Propositions/Types $\endgroup$ – Marc Hamann Apr 3 '11 at 16:50
  • 1
    $\begingroup$ Another related discussion: Classification of Lambda Calculi $\endgroup$ – Marc Hamann Apr 3 '11 at 17:17
  • $\begingroup$ Found another nice article here scientopia.org/blogs/goodmath/2009/11/17/… $\endgroup$ – Rehno Lindeque Apr 4 '11 at 16:35
  • 1
    $\begingroup$ 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" $\endgroup$ – Tobias Raski Apr 4 '11 at 21:30
  • 1
    $\begingroup$ Someone should write an answer from a Homotopy Type Theory point of view. $\endgroup$ – Robin Green Apr 9 '11 at 22:01
20
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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.... $\endgroup$ – Rehno Lindeque Apr 4 '11 at 14:56
  • 1
    $\begingroup$ 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. $\endgroup$ – Dave Clarke Apr 4 '11 at 17:07
  • $\begingroup$ 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"? $\endgroup$ – Rehno Lindeque Apr 4 '11 at 22:47
  • 3
    $\begingroup$ 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. $\endgroup$ – Charles Stewart Apr 5 '11 at 8:24
  • $\begingroup$ @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. $\endgroup$ – Marc Hamann Apr 5 '11 at 15:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.