Thanks for the clear explanation, oleg. -- ryan
On Sat, Jan 30, 2010 at 12:44 AM, <o...@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? > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe