Set-theoretic Types: Brief Intro and Some Base Types

Summary:

• 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$).

(For a more detailed introduction to working with these sorts of types I would recommend taking a look at "A Gentle Introduction to Semantic Subtyping" by Guiseppe Castagna and Alain Frisch and Giuseppe Castagna's unpublished manuscript "Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers)". This blog post was largely motivated by those works.)

Why Semantic Subtyping?

Standard (i.e. syntactic) subtyping is simple and often straightforward to implement. For example, here are standard subtyping inference rules for reflexivity, products, and unions which can be written almost verbatim in the implementation of a type system:

$$ \overline{\tau <: \tau} $$ $$ \frac{\tau_1 <: \sigma_1 \quad \tau_2 <: \sigma_2} {(\tau_1 \times \tau_2) <: (\sigma_1 \times \sigma_2)} $$ $$ \frac{\tau_1 <: \sigma \quad \tau_2 <: \sigma} {(\tau_1 \vee \tau_2) <: \sigma} $$ $$ \frac{\tau <: \sigma_1} {\tau <: (\sigma_1 \vee \sigma_2)} \quad \frac{\tau <: \sigma_2} {\tau <: (\sigma_1 \vee \sigma_2)} $$

These rules, however, do not allow us to derive the following true statement:

$$ ((Int \vee True) \times False) <: ((Int \times False) \vee (True \times False)) $$

This stems from the fact that such syntactic subtyping rules are sound but not complete, i.e. they are valid rules of inference, but we cannot prove all valid subtyping statements with them.

To achieve completeness, our treatment of the subtyping relation $ \tau <: \sigma $ will require a semantic treatment. We will interpret types as subsets of some model, and the subtyping question will then be a matter of deciding set inclusion for the respective interpretations: $[\![\tau]\!] \subseteq [\![\sigma]\!]$. Put more simply, if set of values described by $\tau$ is a subset of the set of values described by $\sigma$, then (and only then) $ \tau <: \sigma $.

Subtyping via a set emptiness check

Algorithms for calculating semantic subtyping often make use of the following equivalence:

$$ [\![\tau]\!] \subseteq [\![\sigma]\!] \equiv [\![\tau]\!] \setminus [\![\sigma]\!] = \emptyset $$

That is, instead of directly checking set inclusion, they check if removing $\sigma$ from $\tau$ produces the empty type.

Boolean Disjunctive Normal Form (DNF) and Satisfiability

Recall that deciding whether a boolean formula is unsatisfiable is simpler when we convert the formula into DNF (i.e. a sum of products of boolean literals, where a literal is a boolean variable or a negated boolean variable):

$$ \bigvee (x_0 \wedge ... \wedge \neg x_i \wedge ...) $$

This is because a DNF formula is unsatisfiable iff each clause is unsatisfiable, and each clause is unsatisfiable iff there are two incompatible literals (e.g. $x$ and $\neg x$). Thus checking for unsatisfiability requires only a linear scan over the DNF formula.

Type DNF and Inhabitation

Perhaps unsurprisingly then, deciding if a type is uninhabited is easier when the type is in DNF. In DNF, each clause in the disjunct is a conjunction of atomic types $ a $ (base types, products, or functions) and/or negated atomic types $ \neg a $:

$$ \bigvee (a_0 \wedge ... \wedge \neg a_i \wedge ...) $$

However, since the various kinds of atoms (base, product, and function) are non-overlapping, clauses with different kinds of atoms can either be (1) eliminated since they are obviously uninhabited (e.g. a value cannot be a pair and a function) or (2) simplified to only contain types of one kind (i.e. if a type is a product, we need not remember also that it is not some function, etc).

We can consider a type in DNF then to only contain clauses with literals of the same kind:

$$ (b_0 \wedge ... \wedge \neg b_i \wedge ...) $$ $$ ((\tau_{0} \times \sigma_{0}) \wedge ... \wedge \neg (\tau_{i} \times \sigma_{i}) \wedge ...) $$ $$ ((\tau_{0} \rightarrow \sigma_{0}) \wedge ... \wedge \neg (\tau_{i} \rightarrow \sigma_{i}) \wedge ...) $$

For a type to be uninhabited, each such conjunction of its DNF must be uninhabited. Since we will be performing this check (subtyping) frequently while type checking programs, we want an efficient representation of DNF types and efficient algorithms for deciding their emptiness.

An individual DNF base type clause

Claim: Any individual clause (i.e. conjunction) in a DNF of base types is equivalent to either $\bot$, $b$, or $\neg(b_0 \vee ... \vee b_n)$.

Base types describe disjoint, non-structural values in a language. Because of this, any individual base type DNF clause can be simplified to one of the following forms:

• $\bot$
• $b$
• $\neg (b_0 \vee ... \vee b_n)$

Let us walk through the possible combinations of base literals in DNF to understand why that is the case:

• Case $(b_0 \wedge ... \wedge b_1 \wedge ...)$ (i.e. a clause with one or more positive literals): Since positive literals are disjoint, if $b_0 \neq b_1$ then the type is equivalent to $\bot$, otherwise if all are equal then it is equivalent to just $b_0$ (and possibly additional, negative literals... but we rule this out in the next case).
• Case: $(b_0 \wedge \neg b_1 \wedge ...)$ (i.e. a clause with a positive literal and negative literals): If $b_0 = b_1$ then the type is equivalent to $\bot$. If $b_0 \neq b_1$ then $ (b_0 \wedge \neg b_1) \equiv b_0 $ since $b_0$ is a subset of the things that are not $b_1$, and thus if there are positive and negative literals the type is either empty or can be simplified to not include any negative literals.
• Case: $(\neg b_0 \wedge \neg b_1 \wedge ...)$ (i.e. a clause with multiple negative literals): using DeMorgan's law we can simplify this form to $\neg (b_0 \vee b_1 \vee ...)$.

DNF base type clauses

Claim: The base portion of a DNF type is equivalent to either $\bot$, $\top$, $(b_0 \vee ... \vee b_n)$, or $\neg(b_0 \vee ... \vee b_n)$.

Since any individual clause in a DNF of base types is equivalent to either $\bot$, $b$, or $\neg(b_0 \vee ... \vee b_n)$ (see above), we just need to verify that these normal forms are closed under disjunction. We do so by examining each possibly combination of normal forms:

• Since $\bot \vee \tau \equiv \tau \vee bot \equiv \tau$, disjunction with $ \bot $ is closed for these forms.
• The union of two positive clauses obviously simply results in a positive union: $$ (b_0 \vee ... \vee b_i) \vee (b_j \vee ... \vee b_n) \equiv (b_0 \vee ... \vee b_i \vee b_j \vee ... \vee b_n)$$
• For the union of a positive and negative clause we can begin by distributing the logical operators: \begin{array}{l} (b_0 \vee ... \vee b_i) \vee \neg(b_j \vee ... \vee b_n) \\ \equiv (b_0 \vee ... \vee b_i) \vee (\neg b_j \wedge ... \wedge \neg b_n) \\ \equiv (((b_0 \vee ... \vee b_i) \vee \neg b_j) \wedge ... \wedge ((b_0 \vee ... \vee b_i) \vee \neg b_n)) \end{array}

  We then simplify each $ ((b_0 \vee ... \vee b_i) \vee \neg b_k) $ in the conjunction.

  If $ b_k \in (b_0 \vee ... \vee b_i) $ then the type is equivalent to $ \top $ and we can drop it from the disjunction.

  If $ b_k \notin (b_0 \vee ... \vee b_i) $ then all we know for certain from the disjunction of the two is $ \neg b_k $, and so we simplify the disjunction to be just $ \neg b_k $.

  Thus after simplifying each clause the conjunction, we are left with a conjunction of negative base literals (specifically those which were in $\neg(b_j \vee ... \vee b_n)$ but not in $ (b_0 \vee ... \vee b_i) $) which is equivalent to the negation of a union of positive literals (i.e. one of our expected normal forms).

• The union of two negative clauses $ \neg(b_0 \vee ... \vee b_i) \vee \neg(b_j \vee ... \vee b_n) $ is equivalent to the negation of the intersection of the clauses. Therefore if the intersection is empty---i.e. if there is no $ b_k $ s.t. $ b_k \in (b_0 \vee ... \vee b_i) $ and $ b_k \in (b_j \vee ... \vee b_n) $---then the result is $\top$, otherwise we get $ \neg(b_k \vee ... \vee b_m) $ (i.e. a negation of the base types $b_k ... b_m$ that appear in both original types).