[Haskell-cafe] Re: Non-termination of type-checking

[oleg at okmij.org]

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


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:
> 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
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?