[Haskell-cafe] Re: Non-termination of type-checking
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Non-termination of type-checking
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
[Haskell-cafe] Re: Non-termination of type-checking
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
[Haskell-cafe] Re: Non-termination of type-checking
On Saturday 30 January 2010 3:44:35 am o...@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).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
On Friday 29 January 2010 2:56:31 am o...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
On Fri, Jan 29, 2010 at 8:56 AM, o...@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)
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Non-termination of type-checking
Le 29 janv. 10 à 02:56, o...@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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
Am Freitag 29 Januar 2010 23:26:28 schrieb Matthieu Sozeau:
Le 29 janv. 10 à 02:56, o...@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
