We explain the technique of systematically deriving absurd terms and apply it to type families. Indeed I should have said that there is no _overt_ impredicative polymorphism in the example posted earlier: it is precisely the impredicative polymorphism that causes the paradox. As everybody noticed, the example was an implementation of the Russell paradox (whose elimination was the goal for the introduction of predicativity). Here is how the `absurd' example was derived. Our goal is to define a recursive (rather than a mere inductive) data type, such as data R = MkR (R -> False) If we have this data type, we can easily obtain the fixpoint combinator, and hence logical inconsistency. But we want to avoid overt recursive type. Therefore, we break the recursive knot, by parameterizing R: data R c = MkR (c -> False) The hope is that we can instantiate the type variable c with R and recover the desired recursive type. The type variable c is thus quantified over the set of types that include the type R being defined. This impredicative polymorphism is essential for the trick. However, instantiating the type variable c with R would be a kind error: c has the kind * and R has the kind *->*. The obvious work-around data R c = MkR (c () -> False) fails: now c has the kind (*->*) but R has the kind (*->*)->*. Again, R is not substitutable for c. If all we have are ordinary data types, we are stuck -- for exactly the same reason that self-application is not expressible in simply-typed lambda-calculus. GADTs come to the rescue, giving us the needed `phase shift'. We can define the datatype as (in pseudo-normal notation) data R (c ()) = MkR (c () -> False) Now we can substitute R for c; alas, the result data R (R ()) = MkR (R () -> False) is not the recursive type. The fix is trivial though: data R (c ()) = MkR (c (c ()) -> False) Now that the method is clear, we derive the absurd term using type functions (lest one thinks we are picking on GADTs). Type families too let us introduce the `phase shift' (on the other side of the equation) and thus bring about the destructive power of impredicativity. Here is the complete code:
{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
data False -- No constructors
data I c = I (c ())
type family Interpret c :: * type instance Interpret (I c) = c (I c)
data R c = MkR (Interpret c -> False)
cond_false :: R (I R) -> False cond_false x@(MkR f) = f x
{- This diverges absurd :: False absurd = cond_false (MkR cond_false) -}
-- Thanks to Martin Sulzmann absurd2 :: False absurd2 = let x = MkR cond_false in cond_false x
Anyhow, I don't particularly find this 'scary', as Haskell/GHC isn't attempting to be an environment for theorem proving, and being able to encode (\x -> x x) (\x -> x x) through lack of logical consistency isn't giving up anything that hasn't already been given up multiple times (through general recursion, error and negative types at least). I agree. Still, it would be nice not to give up logical consistency one more time. More interesting is to look at the languages that are designed for theorem proving. How many of them have impredicative
It seems likely `absurd' diverges in GHCi is because of the GHC inliner. The paper about secrets of the inliner points out that the aggressiveness of the inliner can cause divergence in the compiler when processing code with negative recursive types. Probably GHCi internally derives the recursive equation when processing the instance R (I R) of the data type R. Dan Doel wrote: polymorphism? Are we certain other features of the language, such as type functions (specifically, case analysis) don't introduce the phase shift that unleashes the impredicativity?