It is easy to conflate impredicativity in type theory with impredicativity in set theory. Many set-theoretic counterexamples, such as the diagonal argument or Russell’s paradox, exist because set theory permits certain constructions that are absent in type theory.
Consequently, Impredicativity does not inherently lead to contradictions; even in dependently typed languages, one must leverage additional constructions to formulate a counterexample.
For instance, if we ignore Type, DataType, and Any, Julia’s type system admits a straightforward set-theoretic interpretation. We can distinguish between two kinds of sets: sets of concrete values (whose elements are constructible Julia objects) and sets for abstract values (such as UnionAll, which represent unions of sets of concrete values). This framework does not encounter issues because the type universe is stratified. Russell’s paradox is impossible here because a Julia object is an element while a type is a set; they are distinct entities, making the self-membership x \in x impossible.
Regarding diagonal arguments: Julia lacks function types in the foundational sense, meaning it lacks the necessary powerset construction to violate cardinality (I think this is what you have in your mind, but you cannot directly reuse system F’s constructions here, as we don’t have higher-ranked functions).
Why, then, do Coq (and other dependently typed languages) or set theory encounter these paradoxes?
There are two primary reasons why these paradoxes emerge in such systems:
- Lack of Stratification: If a definition is not well-founded or stratified, paradoxes are more likely to arise. Set theory is essentially untyped, which facilitates the creation of self-referential loops such as x \in x. This is impossible in most statically typed languages, as they typically do not treat types as first-class values in a way that allows such circularity.
- Non-Constructibility: Paradoxes often stem from definitions that are not inherently constructible.
In Coq, for example, the system utilizes two distinct types of universes:
- A single impredicative, non-constructible universe called Prop.
- A hierarchy of predicative, constructible universes (\text{Set}_i), where each level \text{Set}_{i+1} is built from the preceding level \text{Set}_i.
The Prop universe admits a straightforward set-theoretic interpretation: a singleton set represents a true proposition, while an empty set represents a false one. This principle is known as proof irrelevance: if one has x : \text{Prop}, then x merely denotes the existence of a valid proof. Although multiple distinct proofs of a proposition may exist, the system does not distinguish between them, hence the singleton set representation.
In this context, function types do not trigger cardinality issues. Because functions are interpreted as logical implications (truth tables for A → B!), they also map to either a singleton or an empty set. Consequently, the system avoids the classical powerset interpretation that would otherwise lead to a violation of Cantor’s theorem.
Therefore, we cannot have strong elimination (pattern matching) within the Prop universe, which would otherwise allow for the destruction of a Prop value. Much like how one cannot analyze the internal structure of a simple boolean truth value, Props are non-constructible; their internal structures are opaque and cannot be analyzed. In summary, a formal contradiction arises only when the following three properties coexist:
Impredicativity + Proof Irrelevance + Strong Elimination = Contradiction
The point is that impredicativity is not inherently problematic; it only results in a contradiction if every possible interpretation is ruled out, but that requires the coexistence of many other powerful constructions.