I was reading Logicomix (a fictionalised account of logic from Frege to Gödel through Russell's eyes) and there was mention about two different versions of types developed by Russell and Whitehead for Principia Mathematica, unramified (first) and ramified. I don't expect that there is too much relation to the modern type theory (or is there?), but I'm curious to know what the difference is between them. In particular, it is stated that unramified types were not sufficient. How so? 


I know the intuitive description of RW's types as a hierarchy of sets, but nothing beyond that. 



Russell and Whitehead's types: ramified and unramified
Yes, this still occurs in modern type theory; in particular, you'll find it in the [calculus of constructions](http://en.wikipedia.org/wiki/Calculus_of_constructions) employed by the [Coq](http://www.lix.polytechnique.fr/coq/) language.


Consider the type called `Prop`, whose inhabitants are logical propositions (which are in turn inhabited by proofs). The type `Prop` does not belong to `Prop` -- this means that `Prop` exhibits **stratification**:



```
Check Prop.
Prop
 : Type

```

However, note that `(forall a:Prop, a)` **does** have type `Prop`. So although `Prop` does not belong to `Prop`, things which *quantify over all of `Prop`* may still belong to `Prop`. So we can be more specific and say that `Prop` exhibits **unramified stratification**.



```
Check (forall a:Prop, a).                                                       
forall a : Prop, a
 : Prop

```

By contrast, consider `Set`, whose inhabitants are datatypes (which are in turn inhabited by computations and the results of computations). `Set` does not belong to itself, so it too exhibits stratification:



```
Check Set.
Set
 : Type

```

Unlike the previous example, things which *quantify over all of `Set`* do not belong to `Set`. This means that `Set` exhibits **ramified stratification**.



```
Check (forall a:Set, a).
forall a : Set, a
 : Type

```

So, in short, "ramification" in Russell's type hierarchy is embodied today by what Coq calls "predicative" types -- that is, all types except `Prop`. If you quantify over a type, the resulting term no longer inhabits that type unless the type was impreciative (and Prop is the only impredicative type).


The higher levels of the Coq universe (`Type`) are also ramified, but Coq hides the ramification indices from you unless you ask to see them:



```
Set Printing Universes.                                                         
Check (forall a:Type, Type).
Type (* Top.15 *) -> Type (* Top.16 *)
 : Type (* max((Top.15)+1, (Top.16)+1) *)

```

Think of `Top.15` as a variable, like $\alpha\_{15}$. Here, Coq is telling you that if you quantify over the $\alpha\_{15}^{th}$ universe to produce a result in the $\alpha\_{16}^{th}$ universe, the resulting term will fall in the $max(\alpha\_{15}+1, \alpha\_{16}+1)^{th}$ universe -- which is at least "one level up" from what you're quantifying over.


Just as it was later discovered that Russell's ramification was unnecessary (for logic), it turns out that predicativity is unnecessary for the purely logical portion of CiC (that is, `Prop`).


