Example of where violation of strict positivity condition in inductive types leads to inconsistency

Question

Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?

Answer 1

It is actually possible to relax strict positivity and remain consistent. For instance, it suffices to only have a positivity condition. That is, we can accept type definitions like

$$ T \triangleq \mu\alpha. (\alpha \to 2) \to 2 $$

where recursive type variables occur to the left of an even number of arrows and retain consistency.

However, theories permitting this sort of inductive type do not have set-theoretic models -- you cannot interpret types as sets and terms as elements of sets. In this case, we are saying that $T$ is isomorphic to its double-powerset (i.e., $T \simeq \mathcal{P}(\mathcal{P}(T))$), and this violates Cantor's theorem.

Since dependent type theories are often used to formalize mathematics, their designers are usually hesitant to add principles which are not compatible with a set-theoretic semantics, even if they are consistent.

EDIT: I'm adding this edit in response to Andrej's question. The type $T$ is consistent if you add it to (say) Agda; there are no problems with it at all. We only have a problem if we combine non-strict positivity with excluded middle.

The intuition for why is safe is (IMO) best seen through the lens of parametricity. In System F, we can show using parametricity that for any definable functor $F$, the type $\mu F \triangleq \forall \alpha.\; (F\alpha \to \alpha) \to \alpha$ is indeed an inductive type.

Now, recall that a definable functor $F$ is a type operator $F : \ast \to \ast$, together with an operator $$\mathrm{map} : \forall \alpha,\beta.\;(\alpha \to \beta) \to F\;\alpha \to F\;\beta$$ satisfying the functoriality conditions (i.e., $\mathrm{map}\;id = id$ and $\mathrm{map}\;f\;\circ \mathrm{map}\;g = \mathrm{map}\;(f \circ g$).

Now, we can define a type operator for the double powerset

$$C = \lambda \alpha.\; (\alpha \to 2) \to 2$$

and because $\alpha$ occurs only positively, we can also define a map operator for it:

$$ map_C = \lambda f : \alpha \to \beta, a' : (\alpha \to 2) \to 2, k : \beta \to 2.\; a' \;(\lambda a:\alpha.\; k\;(f\;a)) $$

So we know that $T = \mu C$ is a legitimate inductive type.