ZFA (1908) had urelements. You can just partition your urelements if you want distinct "types". Union across those would be disjoint, but within would be standard set union. Even in type theory you have Church VS Curry style as to whether you consider terms as inheritly belonging to a type.
> You can just partition your urelements if you want distinct "types". Union across those would be disjoint, but within would be standard set union.
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.
1. Haven't read too deeply, but aren't we working with FOL in this type system anyway (Well, Henkin semantics of HOL, I believe)
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.
