Algebraic data types - unions

Are there any programming languages where algebraic data types can be expressed not only by using intersection and disjoint union but also a standard set union (intersection + disjoint union)?

Do such types even make sense?

If so, could you provide practical example of use?

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.

StackExchange Computer Science Q#64099, answer score: 5