Impredicativity + injectivity + type case analysis = inconsistency (Russell paradox)

Matthieu Sozeau has started the discussion on Haskell Cafe on January 27, 2010, describing the divergence in the type checker encountered while encoding a recently found Coq paradox in Haskell, using GADTs and Rank2Types. The follow-up messages have distilled the problem, which turns out different from the one on Coq and Agda. This web page, expanding on the message posted on January 30, 2010, explains the technique of systematically deriving absurd terms and demonstrates it on three examples of type case analysis, with GADTs and with type families. I thank Dan Doel, Daniel Fischer and Martin Sulzmann for their comments during the January 2010 discussion. I am very grateful to Stephanie Weirich for further discussions and especially for her explanations of injectivity in System FC.

• Background
• Deriving absurd with GADTs
• Deriving absurd with standard injectivity
• Deriving absurd with data families
• Deriving absurd with type families

Background

For ease of reference, we recall the three components of the paradox: impredicativity, injectivity of type constructors, and case analysis on types.

A definition is predicative if it is not circular. An impredicative definition, in contrast, indirectly refers to the object being defined by quantifying over the domain that includes the object. Here is an example of a predicative Haskell definition of the type P, and of a sample term prd of that type:

     type P = forall a. a -> [a]
     prd :: P
     prd x = [x]

The type P is polymorphic; the quantified variable a (implicitly) ranges over non-polymorphic types (monotypes) and therefore cannot be instantiated with P. For that reason we cannot apply prd to itself. The apparent self-application in

     tprd1 = case prd prd of [f] -> f True

is illusory: we apply the polymorphic function prd not to itself but to an instance of itself. Therefore, the following definition is ill-typed:

     tprd2 = case prd prd of [f] -> (f True, f 'a')
        Error: Couldn't match expected type `Bool' with actual type `Char'

Haskell also permits impredicative definitions, like the following:

     newtype I = I{unI :: forall a. a -> [a]}
     imprd :: I
     imprd = I (\x -> [x])
     tim = case unI imprd imprd of [I f] -> (f True, f 'a')

The type I is a monotype and so the quantified type variable a in I's definition can be instantiated with I itself. The well-typed term tim demonstrates exactly such an instantiation.

Injectivity of type constructors means that a type constructor T (defined by a data declaration) gives distinct types when applied to distinct arguments. Contrapositively:

     T a ~ T b  implies a ~ b

where ~ is the symbol for type equality in Haskell. For example, if two lists have the same type, their elements have the same type.

Haskell has type functions that do the case analysis on types, extracting their components. Such type functions can be implemented via functional dependencies, GADTs, type or data families. The type family below

     type family Elem x :: *
     type instance Elem [a]       = a
     type instance Elem (Maybe a) = a

extracts the element type from the list or the option type. Incidentally, Elem is non-injective: it maps distinct types [Int] and Maybe Int to the same result Int.

References

Thierry Coquand: Type Theory
The Stanford Encyclopedia of Philosophy (Spring 2010 Edition), Edward N. Zalta (ed.)
< http://plato.stanford.edu/archives/spr2010/entries/type-theory/ >
The article gives the detailed analysis of Russell paradox and its avoidance in the simple type theory. Although the simple type theory forbids self-application, it permits circular, impredicative definitions. The article discusses the ramified type theory that avoids circularity altogether, at the expense of expressivity. There is a fine balance in permitting some forms of circularity while maintaining consistency.

Deriving absurd with GADTs

This warm-up section describes the technique of systematically deriving absurd terms and proving False. For the sake of explanation, we rely here on a stronger property than injectivity, namely, System FC's Fst, which is available in some versions of GHC. The next section adjusts the derivation to use just the standard injectivity. Let us first see the result, the complete code for the well-typed but divergent term absurd defined without either value or type recursion.

     {-# LANGUAGE GADTs, KindSignatures, EmptyDataDecls #-}
     data False				-- No constructors
     
     data R :: * -> * where
       MkR :: (c (c ()) -> False) -> R (c ())
     
     cond_false :: R (R ()) -> False
     cond_false x@(MkR f) = f x
     
     -- May cause divergence in the type checker
     absurd :: False
     absurd = cond_false (MkR cond_false)
     
     absurd2 :: False
     absurd2 = let x = MkR cond_false in cond_false x

The term absurd may cause the infinite loop in the type checker in old versions of GHC. The term absurd2, re-written to thwart aggressive inlining, is more widely acceptable. The code works with versions of GHC before 7.4, and may start working again with GHC 7.8.

The code was derived as follows. Our goal is to encode Russell paradox by defining a recursive (rather than a mere inductive) data type, such as

     data R = MkR (R -> False)

The type R -> False can be regarded as the negation of R. The value of R then carries the proof of its own non-existence. From a different point of view, a recursive data type such as R lets us express the fixpoint combinator, and hence attain the logical inconsistency. The above definition of R however relies on the type-level recursion, which we want to avoid. We break the recursive knot, by parameterizing R:

     data R c = MkR (c -> False)

We hope to instantiate the type variable c with R and recover the desired recursive type. Impredicativity, defining the class of types R c in terms of the class of all types, which includes R c itself, is crucial. However, we cannot instantiate c with R since the two have different kinds: c has the kind * and R is the type constructor, of the kind *->*. A naive work-around

     data R c = MkR (c () -> False)

fails: although c now has the kind *->*, R has the kind (*->*)->* and not substitutable for c. With the ordinary data types, we are stuck -- for exactly the same reason that self-application is not expressible in simply-typed lambda-calculus. Impredicativity per se does not lead to inconsistency.

GADTs come to the rescue, giving us the needed `phase shift'. In the raw GADT notation,

     data R c' = c' ~ c () => MkR (c () -> False)

Now c', conditioned to be of the form c (), is of the kind *. The type variable c is of the kind *->*; R is of the same kind and so is substitutable for c. Thus the data type instance R (R ()) (when c' is instantiated with R () and c becomes R) has the value MkR (R () -> False). That is not quite the paradox: the value of the type R (R ()) carries the negation of just R (). But the mismatch is easy to fix:

     data R c' = c' ~ c () => MkR (c (c ()) -> False)

Instantiating c with R and noting that R (R ()) coincides with R c' when c' is R () give us the desired vicious circle.

In the definition of cond_false, the argument x must have the type R (c ()) because it is constructed by the data constructor MkR. On the other hand, the type signature of cond_false ascribes to x the type R (R ()). We obtain the equation R (R ()) ~ R (c ()), which the injectivity of R simplifies to R () ~ c (). To proceed further, we need the System FC property called Fst: a x ~ b y entails a ~ b, which gives the desired instantiation R ~ c. The property Fst was removed from GHC 7.4, but is reportedly on its way back. The example will work again then. The error message by GHC 7.4 is quite informative, validating our analysis:

     Could not deduce (c ~ R)
     from the context (R () ~ c ())
       bound by a pattern with constructor
                  MkR :: forall (c :: * -> *). (c (c ()) -> False) -> R (c ()),
                in an equation for `cond_false'

Deriving absurd with standard injectivity

The previous section explained the derivation of the absurd term that witnesses False using injectivity and the property Fst. This section removes the dependence on Fst. The adjusted code compiles with any recent version of GHC. Further, Stephanie Weirich showed that the example can be translated to Coq, with injectivity added as an axiom.

Recall Fst means a x ~ b y entails a ~ b whereas the weaker, standard injectivity (which could be called Snd or Nth) leads from T a ~ T b to a ~ b. We relied on Fst to get c ~ R from c () ~ R (). To avoid Fst and use only injectivity, we need to ``shift'' c into the argument position -- for example, replace c () with J c for some injective type constructor J. As usual, the hardest part was stating exactly what we want. Getting it is easy: here is the complete code.

     {-# LANGUAGE GADTs, KindSignatures, EmptyDataDecls #-}
     
     data False                         -- No constructors
     
     data J c = J (c ())
     
     data R :: * -> * where
       MkR :: (c (J c) -> False) -> R (J c)
     
     cond_false :: R (J R) -> False
     cond_false x@(MkR f) = f x
     
     absurd :: False
     absurd = cond_false (MkR cond_false)

In the definition cond_false, the argument x must have the type R (J c) since it is constructed by MkR. The ascription of the signature R (J R) gives the equality R (J c) ~ R (J R), from which we obtain the desired c ~ R after two applications of injectivity. Stephanie Weirich has pointed out that the System FC term for cond_false in the output of the GHC simplifier indeed shows two applications of injectivity-induced coercions (called Nth).

With Ex Falso Quodlibet, the example can be made more absurd:

     {-# LANGUAGE GADTs, KindSignatures #-}
     
     data J c = J (c ())
     
     data R :: * -> * -> * where
       MkR :: (c (J c) -> a) -> R a (J c)
     
     cond_false :: R a (J (R a)) -> a
     cond_false x@(MkR f) = f x
     
     absurd :: a
     absurd = cond_false (MkR cond_false)

Truly, every type is populated, and absurd is the evidence of it.

Deriving absurd with data families

GADTs are not the only way to define non-parametric data types -- polymorphic data types with case analysis on the argument type. Data families is another approach. The absurd example is straightforward to re-write for data families. Here is the complete code.

     {-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
     data False				-- No constructors
     data J c = J (c ())
     
     data family R c
     data instance R (J c) = MkR (c (J c) -> False)
     
     cond_false :: R (J R) -> False
     cond_false x@(MkR f) = f x
     
     absurd :: False
     absurd = cond_false (MkR cond_false)

Deriving absurd with type families

Data families can be factored out into ordinary data type and the case analysis on the index type. Type families do the case analysis. Here is yet another version of the absurd code.

     {-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
     data False				-- No constructors
     
     data J c = J (c ())
     
     type family Interpret t :: *
     type instance Interpret (J c) = c (J c)
     
     data R c = MkR (Interpret c -> False)
     
     cond_false :: R (J R) -> False
     cond_false x@(MkR f) = f x
     
     absurd :: False
     absurd = cond_false (MkR cond_false)

As an explanation, let us build the type derivation for False, noting where impredicativity, injectivity and type case analysis come into play. The pattern x@(MkR f) in the definition of cond_false gives the following type assignments, where a is a not yet determined type:

     x :: R a
     f :: Interpret a -> False

The definition of the class of data types R c is impredicative since c ranges over all types and can be instantiated with a member of the R class itself. The type signature of cond_false and the term MkR cond_false make such an instantiation. The signature of cond_false, which ascribes to x the type R (J R), gives the equality R a ~ R (J R). The injectivity of the type constructor R turns the equality to a ~ J R. Substituting J R for a in the type of f gives rise to Interpret (J R), which fits the type family instance and hence improves to R (J R). The improvement had to deconstruct the type J R and extract its component. After the improvement, the argument type of f matches the type of x and the type checking of cond_false succeeds. In absurd, the argument type of cond_false requires that MkR cond_false be of the type R (J R), yielding by injectivity, the instantiation of c to J R. After applying the type family instance, the type checker concludes that MkR cond_false, and absurd are well-typed.

Last updated November 5, 2012

Converted from HSXML by HSXML->HTML