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

[Dan Doel]

On Saturday 30 January 2010 3:44:35 am oleg at 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).