9
$\begingroup$

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?

$\endgroup$
10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Can we come up with an example which creates an inconsistency all by itself? Your example is inconsistent if we also assume (enough) excluded middle. $\endgroup$ – Andrej Bauer Apr 2 '14 at 9:24
  • $\begingroup$ Another reason is that we can add the FAN theorem to Agda, after which we can prove that the type in question is (isomorphic to) natural numbers. $\endgroup$ – Andrej Bauer Apr 2 '14 at 10:22
  • $\begingroup$ I am thinking $\mu \alpha . (\alpha \to 2) \to \alpha$ should be pretty bad. $\endgroup$ – Andrej Bauer Apr 2 '14 at 10:23
  • 1
    $\begingroup$ Ah, I misunderstood the question -- the point is that strict positivity is a sufficient but not necessary condition. Your example (with an actual negative occurence) is inconsistent. $\endgroup$ – Neel Krishnaswami Apr 2 '14 at 11:07
  • $\begingroup$ Yeah, I just realized that. My example doesn't hold water. $\endgroup$ – Andrej Bauer Apr 2 '14 at 12:08

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.