The type &lt;t1,…, tn&gt; is the type of a relation among entities of types t1,…, tn. But, for simplicity, we will interpret this as the type of a function that takes these entities to a proposition. (Note that when n = 0, then the empty type, &lt; &gt;, is the type for propositions.) This definition incorporates the idea of a well-founded structure. There are no cycles here. We cannot have a function that takes as an argument a function of the same or higher type. Thus, simple type theory bans the sort of self-application that gives rise to Russell's paradox.