- Semantic subtyping allows for a more complete treatment of subtyping.
- Keeping types in DNF can be convenient for checking emptiness.
- The base type portion of a DNF type is either $\top$, $\bot$, $(b_0 \vee ... \vee b_n)$ or $\neg(b_0 \vee ... \vee b_n)$.
Set-theoretic Types
Here is a simple grammar for types with set-theoretic constructors:
\begin{array}{l c l l} \tau , \sigma & ::= & b & Base \, type \, (e.g. \, Int,\, Str,\, etc) \\ & \mid & \tau \times \tau & Product \\ & \mid & \tau \rightarrow \tau & Function \\ & \mid & \tau \vee \tau & Union \\ & \mid & \tau \wedge \tau & Intersection \\ & \mid & \neg \tau & Negation \\ & \mid & \top & Anything \end{array}In other words, it includes some simple types as well as set-theoretic operators that allow us to express logical "or" (union), "and" (intersection), and "not" (negation) along with top and bottom types $\top$ and $\bot$ (which is short for $\neg \top$).
