In which sense would partitioning urelements lead to something like types? This sounds somewhat like many sorted logic, which is only as expressive as first-order logic, not higher-order logic / simple type theory: https://plato.stanford.edu/entries/logic-many-sorted/
> Even in type theory you have Church VS Curry style as to whether you consider terms as inheritly belonging to a type.
Not sure what the difference is here.
2. I guess the major semantic difference is that in one, you define a family of PERs for terms in a given type, giving each type separate notion of equality. In the other you define equality over all terms and types are just a predicates on terms. I honestly am not well versed enough in logic to understand what it means in that sense.
If you want a more expressive logic, use a language with dependant types. Although I wish to see more powerful type systems become more mainstream, I don't expect every language to aim for that.