# 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?

• If you consider a tuple an "algebraic data type" then SQL supports such operations: en.wikipedia.org/wiki/Set_operations_(SQL) – Math1000 Oct 1 '16 at 16:03
• I'm not sure exactly what you're asking, but types aren't sets. If we tried to express product and sum types as set intersection and union, we could not build a valid semantics for the languages (assuming the language is sufficiently general). – gardenhead Oct 1 '16 at 18:19
• @gardenhead What OP is talking about absolutely exists, they're called set theoretic types, and they're not common, but have a well developed theory behind them. – jmite Oct 1 '16 at 19:54

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.