> In all popular languages that support "sum types" we just call them "unions."

When I was doing research on type theory in PL, there was an important distinction made between sum types and unions, so it’s important not to conflate them. Union types have the property that Union(A, A) = A, but the same doesn’t hold for sum types. Sum types differentiate between each member, even if they encapsulate the same type inside of it. A more appropriate comparison is tagged unions.

What you are calling Union type is not what GP is talking about.

So, disjoint union in set theory terms?

If I understand correctly .