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

[Ryan Ingram]

Thanks for the clear explanation, oleg.

  -- ryan

On Sat, Jan 30, 2010 at 12:44 AM,  <oleg at okmij.org> wrote:
>
> 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?
>
>