On Saturday 30 January 2010 3:44:35 am oleg@okmij.org wrote:
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.
I've even observed your prior code hang when loading into GHCi, though. Does inlining get done even for byte code, with no -O?
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?
Coq has an impredicative universe of propositions, and Agda has a --type-in- type option (which is definitely inconsistent), allowing both to encode your systematically derived type. However, neither allow one to actually well type (\x -> x x) (\x -> x x) by this method. In Agda: {-# OPTIONS --type-in-type --injective-type-constructors #-} module Stuff where data False : Set where data Unit : Set where unit : Unit data R : Set → Set where r : (F : Set → Set) → (F (F Unit) → False) → R (F Unit) w : R (R Unit) → False w x with R Unit | x ... | ._ | r F f = {! !} The "with" stuff can be ignored; that's required get Agda to allow matching on x for some reason. Anyhow, we need to fill in the hole delimited by the {! !} with something of type False, but what we have are: x : R (R Unit) f : F (F Unit) -> False And I'm pretty sure that there's no way to convince Agda that F = R, or something similar, because, despite the fact that Agda has injective type constructors like GHC (R x = R y => x = y), it doesn't let you make the inference R Unit = F Unit => R = F. Of course, in Agda, one could arguably say that it's true, because Agda has no type case, so there's (I'm pretty sure) no way to write an F such that R T = F T, but R U /= F U, for some U /= T. But, in GHC, where you *do* have type case, and *can* write functions like the above, GHC lets you infer that R = F anyway, and throws type errors when trying to build elements of R (T ()) for T () = R () but T /= R. I'm relatively sure Coq is in the same boat as Agda. I've successfully defined R above as a Prop, using impredicativity, but I'm pretty sure you'll run into the same difficulty trying to write w there (but I don't know Coq well enough to give a demonstration). Coq doesn't give injectivity of type constructors by fiat, which is good, because it can be used with impredicativity to write other paradoxes (just not the one above). Agda has the injectivity,* but not the impredicativity. Also, this all originally came (I believe) from the Agda mailing list, where someone demonstrated that injectivity of type constructors is inconsistent with a certain version of the law of the excluded middle.** However, the paradox above seems to be unique to GHC (among the three), which is rather odd. -- Dan * Injectivity of type constructors is now optional in Agda, turned on by the flag you can see above. ** Injectivity of type constructors allows you to write a proof of: ¬ (∀ (P : Set1) → P ∨ ¬ P) there was some concern raised, because in intuitionistic logic, one can prove: ∀ (P : Set1) → ¬ ¬ (P ∨ ¬ P) But, the above two propositions aren't contradictory, because one can't move the quantifier past the negations as one could in classical logic. Coq in fact allows one to prove something similar to the first proposition with -- impredicative-set, which led to that being off by default (so that one could take excluded middle as an axiom and do classical reasoning without (hopefully) introducing inconsistency).