The SEP entry on second order or higher logic in passing say that countable order logic is type theory. My impression that this is the type theory of the Principia (I may be wrong here).
There is type theory in contemporary logic and computer-science, for example you have the typed lambda calculus, or typed first order logic.
It only just occurred to me that this may be referring to the same concept - mainly because the 2nd order logic with Henkin semantics is equivalent to typed first order logic. This gives the impression that one can fold down the hierarchy of predicates in countable order logic to a kind of type theory.
Is this on the right track?