Я, честно признаться, плохо понял вопрос. Существует масса систем, в которых любой терм типизируем. Самая простая из них - каждому терму приписывается тип (I am a lambda-term).

Безотносительно к этому каждая "хорошая" система типов хороша тем, что позволяет на своём языке делать какие-то полезные содержательные утверждения о программах.