3
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ If you consider a tuple an "algebraic data type" then SQL supports such operations: en.wikipedia.org/wiki/Set_operations_(SQL) $\endgroup$ – Math1000 Oct 1 '16 at 16:03
  • 1
    $\begingroup$ 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). $\endgroup$ – gardenhead Oct 1 '16 at 18:19
  • 2
    $\begingroup$ @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. $\endgroup$ – jmite Oct 1 '16 at 19:54
5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.