Algebraic data types - unions
Yes, these type systems exist. They're generally referred to as "Set-theoretic Type Systems", and there's a good rundown of them here. They've been extended a lot, particularly with regards to subtyping and datasort-refinement types. 

For a practical application of them, checkout their use in TypeScript.

Basically, union types correspond to untagged unions, and intersection types are a single value that matches two types. So we have rules that look like this:


If $v : T_1$, then $v : T_1 \cup T_2$ for any $T_2$
If $v : T_1$ and $v : T_2$, then $v : T_1 \cap T_2$


These are both commutative, so there's a symmetric union rule.

Note the difference between normal types: the unions here are untagged, and we have very little information when using a value of a union type, since we have no runtime way of determining which half of the union it is.

Likewise, a value matching an intersection type is not a pair, it's a single value that happens to typecheck against both of the types in the intersection.

Under this formulation, we can treat polymorphic and existential types as infinite intersections and unions:


$\forall a \ldotp T$ is $\bigcap_{S \in TYPE} [S/a]T$
$\exists a \ldotp T$ is $\bigcup_{S \in TYPE} [S/a]T$


That is, if a value typechecks against a polymorphic type, then it checks against any instance of that type. And if a value typechecks against an existential type, there must be some concrete type that it typechecks against. 

As you might expect, introducing these usually makes type inference undecidable, though there is a lot of research going on in this area that I will not claim to be an expert in.