Unions, intersections and negations are available in types as well and are by no means exclusive to sets. The distinguishing feature of a set vs type is that a value belongs to just one type while it can belong to several sets.
Unions, intersections and negations are available in types as well and are by no means exclusive to sets. The distinguishing feature of a set vs type is that a value belongs to just one type while it can belong to several sets.
Types do not inherently have any such restrictions. A value can belong to several types. In fact, if you posit types to have union, that necessarily follows.
I think they do, and as you mentioned you can explicitly remove such a restriction. Sets and types are once again two different kinds of objects in mathematical theory, and a set-theoretic type doesn’t seem to be based either on set theory or type theory.
If types have unions/intersections/negations, as you originally seemed to imply, then “a value belongs to just one type” is false (if x is of type A then it’s also of type A ∪ B for any B).
If they don’t unless you add them to “explicitly remove such a restriction”, then that means you’re making types more set-like (set-theoretic).
In strict “type theory”, it’s the latter: types don’t have unions (in the sense that set-theoretic types do). There are sum types, which are different.