  In this paper we examine the natural interpretation of a ramified type
hierarchy into Martin-L\"of type theory with an infinite sequence of universes.
It is shown that under this predicative interpretation some useful special
cases of Russell's reducibility axiom are valid, namely functional
reducibility. This is sufficient to make the type hierarchy usable for
development of constructive mathematics. We present a ramified type theory
suitable for this purpose. One may regard the results of this paper as an
alternative solution to the problems of Russell's theory, which avoids
impredicativity, but instead imposes constructive logic. The intuitionistic
ramified type theory introduced here, also suggests that there is a natural
associated notion of predicative elementary topos.
