Re: Non-termination of type-checking
Here is a bit more simplified version of the example. The example has no value level recursion and no overt recursive types, and no impredicative polymorphism. The key is the observation, made earlier, that two types c (c ()) and R (c ()) unify when c = R. Although the GADTs R c below is not recursive, when we instantiate c = R, it becomes recursive, with the negative occurrence. The trouble is imminent. We reach the conclusion that an instance of a non-recursive GADT can be a recursive type. GADT may harbor recursion, so to speak. The code below, when loaded into GHCi 6.10.4, diverges on type-checking. It type-checks when we comment-out absurd. {-# LANGUAGE GADTs, EmptyDataDecls #-} data False -- No constructors data R c where -- Not recursive R :: (c (c ()) -> False) -> R (c ()) -- instantiate c to R, so (c (c ())) and R (c ()) coincide -- and we obtain a recursive type -- mu R. (R (R ()) -> False) -> R (R ()) cond_false :: R (R ()) -> False cond_false x@(R f) = f x absurd :: False absurd = cond_false (R cond_false)
On Friday 29 January 2010 2:56:31 am oleg@okmij.org wrote:
Here is a bit more simplified version of the example. The example has no value level recursion and no overt recursive types, and no impredicative polymorphism. The key is the observation, made earlier, that two types c (c ()) and R (c ()) unify when c = R. Although the GADTs R c below is not recursive, when we instantiate c = R, it becomes recursive, with the negative occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False -- No constructors
data R c where -- Not recursive R :: (c (c ()) -> False) -> R (c ())
-- instantiate c to R, so (c (c ())) and R (c ()) coincide -- and we obtain a recursive type -- mu R. (R (R ()) -> False) -> R (R ())
cond_false :: R (R ()) -> False cond_false x@(R f) = f x
absurd :: False absurd = cond_false (R cond_false)
This example is pretty weird in my view. For instance, consider: data S x type family T x :: * type family T () = R () type family T (R ()) = S () s'elim :: S x -> False s'elim x = undefined -- case x of {} what :: T (T ()) -> False what = s'elim Now, we have T () ~ R (), and T (T ()) ~ S (R ()), so R (T ()) ~ R (R ()), no? And T :: * -> *, so it should be an acceptable argument to R. So, one would expect that I could write: r :: R (R ()) -- R (T ()) r = R what However, neither of those signatures for r goes through. With the second, I get a complaint that: Couldn't match expected type `S ()' against inferred type `()' Expected type: S (S ()) Inferred type: T (T ()) though I'm not quite sure how it gets that error. With the R (R ()) choice, I get: Couldn't match expected type `R (R ())' against inferred type `T (T ())' NB: `T' is a type function, and may not be injective but the injectivity GHC seems to be relying on isn't F x ~ F y => x ~ y, but: f T ~ g T => f ~ g or injectivity of ($ ()) in this case, so to speak. But this seems like a significantly weirder thing to take for granted than injectivity of type constructors. I suppose it's sufficient to limit c (in the constructor R's definition) to accept only data type constructors, but that's significantly more limiting than I'd expect to be the case (although, it does appear to be what GHC does). 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). Non-termination of type checking is undesirable, of course. -- Dan
On Fri, Jan 29, 2010 at 8:56 AM,
Here is a bit more simplified version of the example. The example has no value level recursion and no overt recursive types, and no impredicative polymorphism. The key is the observation, made earlier, that two types c (c ()) and R (c ()) unify when c = R. Although the GADTs R c below is not recursive, when we instantiate c = R, it becomes recursive, with the negative occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False -- No constructors
data R c where -- Not recursive R :: (c (c ()) -> False) -> R (c ())
-- instantiate c to R, so (c (c ())) and R (c ()) coincide -- and we obtain a recursive type -- mu R. (R (R ()) -> False) -> R (R ())
cond_false :: R (R ()) -> False cond_false x@(R f) = f x
absurd :: False absurd = cond_false (R cond_false)
GHC (the compiler terminates) The following variants terminate, either with GHCi or GHC, absurd1 :: False absurd1 = let x = (R cond_false) in cond_false x absurd2 = R cond_false absurd3 x = cond_false x absurd4 :: False absurd4 = absurd3 absurd2 This suggests there's a bug in the type checker. If i scribble down the type equation, I can't see why the type checker should loop here. -Martin
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Le 29 janv. 10 à 02:56, oleg@okmij.org a écrit :
Here is a bit more simplified version of the example. The example has no value level recursion and no overt recursive types, and no impredicative polymorphism. The key is the observation, made earlier, that two types c (c ()) and R (c ()) unify when c = R. Although the GADTs R c below is not recursive, when we instantiate c = R, it becomes recursive, with the negative occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False -- No constructors
data R c where -- Not recursive R :: (c (c ()) -> False) -> R (c ())
Thanks Oleg, that's a bit simpler indeed. However, I'm skeptical on the scoping of c here. Correct me if I'm wrong but in R's constructor [c] is applied to () so it has to be a type constructor variable of kind :: * -> s. But [c] is also applied to [c ()] so we must have s = * and c :: * -> *. Now given the application [R (c ())] we must have [R :: * -> *]. Then in [data R c] we must have [c :: *], hence a contradiction? My intuition would be that the declaration is informally equivalent to the impredicative: data R (c :: *) where R :: forall c' :: * -> *, (c' (c' ()) -> False) -> R (c' ()). -- Matthieu
On Friday 29 January 2010 5:26:28 pm Matthieu Sozeau wrote:
data R (c :: *) where R :: forall c' :: * -> *, (c' (c' ()) -> False) -> R (c' ()).
This is what the data declaration is. The c on the first line and the c on the second line are unrelated. It's sort of an oddity of GADT declarations; variables used between the 'data' and 'where' are just placeholders. With KindSignatures enabled, one could also write: data R :: * -> * where R :: (c (c ()) -> False) -> R (c ()) or explicitly quantify c in the constructor's type. That confused me at first, as well. -- Dan
Am Freitag 29 Januar 2010 23:26:28 schrieb Matthieu Sozeau:
Le 29 janv. 10 à 02:56, oleg@okmij.org a écrit :
Here is a bit more simplified version of the example. The example has no value level recursion and no overt recursive types, and no impredicative polymorphism. The key is the observation, made earlier, that two types c (c ()) and R (c ()) unify when c = R. Although the GADTs R c below is not recursive, when we instantiate c = R, it becomes recursive, with the negative occurrence. The trouble is imminent.
We reach the conclusion that an instance of a non-recursive GADT can be a recursive type. GADT may harbor recursion, so to speak.
The code below, when loaded into GHCi 6.10.4, diverges on type-checking. It type-checks when we comment-out absurd.
{-# LANGUAGE GADTs, EmptyDataDecls #-}
data False -- No constructors
data R c where -- Not recursive R :: (c (c ()) -> False) -> R (c ())
Thanks Oleg,
that's a bit simpler indeed. However, I'm skeptical on the scoping of c here.
The c in "data R c" has nothing to do with the c in "R :: (c (c ()) -> False) -> R (c ())" It would probably have been less confusing to declare it data R :: * -> * where R :: (c (c ()) -> False) -> R (c ())
Correct me if I'm wrong but in R's constructor [c] is applied to () so it has to be a type constructor variable of kind :: * -> s. But [c] is also applied to [c ()] so we must have s = * and c :: * -> *. Now given the application [R (c ())] we must have [R :: * -> *]. Then in [data R c] we must have [c :: *], hence a contradiction?
My intuition would be that the declaration is informally equivalent to the impredicative:
data R (c :: *) where R :: forall c' :: * -> *, (c' (c' ()) -> False) -> R (c' ()).
-- Matthieu
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
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
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: 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?
Thanks for the clear explanation, oleg.
-- ryan
On Sat, Jan 30, 2010 at 12:44 AM,
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.
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
Dan Doel wrote: 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?
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).
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.
It's easy to construct an F that is different from R but agrees with R for the case of Unit: F = λ _ -> R Unit So there's a good reason why Agda doesn't let F and R unify: it would really be completely wrong. Stefan
participants (7)
-
Dan Doel -
Daniel Fischer -
Martin Sulzmann -
Matthieu Sozeau -
oleg＠okmij.org -
Ryan Ingram -
Stefan Monnier