 In many contexts of reasoning and computing it is natural to distinguish between different kinds of objects. The way this distinction is introduced is by requiring that certain formulas, functions, or relations accept arguments or permit substitution only of some kinds of objects rather than others. We might require, for example, that addition + take numbers as arguments. The effect of this restriction is to forbid, say, the addition of 5 and the identity function  \(\lambda x.x\).(4).  Regimenting objects into types is also the idea behind the passage from (unsorted, or one-sorted) first-order logic to many-sorted first-order logic. (See (Enderton, 2001) and (Manzano, 2005) for more about many-sorted first-order logic.) As it stands, the \(\lambda\)-calculus does not support this kind of discrimination; any term can be applied to any other term.