
On Saturday 30 January 2010 3:44:35 am [email protected] 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 typein
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 typeintype injectivetypeconstructors #}
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 
impredicativeset, 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).
_______________________________________________
HaskellCafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskellcafe

