Non-termination of type-checking
Dear Haskellers, while trying to encode a paradox recently found in Coq if one has impredicativity and adds injectivity of type constructors [1] I stumbled on an apparent loop in the type checker when using GADTs, Rank2Types and EmptyDataDecls.
{-# OPTIONS -XGADTs -XRank2Types -XEmptyDataDecls #-}
module Impred where
The identity type
data ID a = ID a
I is from (* -> *) to *, we use a partial application of [ID] here.
data I f where I1 :: I ID
The usual reification of type equality into a term.
data Equ a b where Eqrefl :: Equ a a
The empty type
data False
This uses impredicativity: Rdef embeds a (* -> *) -> * object into R x :: *.
data R x where Rdef :: (forall a. Equ x (I a) -> a x -> False) -> R x
r_eqv1 :: forall p. R (I p) -> p (I p) -> False r_eqv1 (Rdef f) pip = f Eqrefl pip
r_eqv2 :: forall p. (p (I p) -> False) -> R (I p) r_eqv2 f = Rdef (\ eq ax -> case eq of -- Uses injectivity of type constructors Eqrefl -> f ax)
r_eqv_not_R_1 :: R (I R) -> R (I R) -> False r_eqv_not_R_1 = r_eqv1
r_eqv_not_R_2 :: (R (I R) -> False) -> R (I R) r_eqv_not_R_2 = r_eqv2
rir :: R (I R) rir = r_eqv_not_R_2 (\ rir -> r_eqv_not_R_1 rir rir)
Type checking seems to loop here with ghc-6.8.3, which is a bit strange given the simplicity of the typing problem. Maybe it triggers a constraint with something above?
-- Loops -- absurd :: False -- absurd = r_eqv_not_R_1 rir rir
[1] http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/4322/focus=... -- Matthieu
The compiler doesn't loop for me with GHC6.10.4; I think GADTs still
had some bugs in GHC6.8.
That said, this is pretty scary. Here's a simplified version that
shows this paradox with just a single GADT and no other extensions.
No use of "fix" or recursion anywhere!
{-# LANGUAGE GADTs #-}
module Contr where
newtype I f = I (f ())
data R o a where R :: (a (I a) -> o) -> R o (I a)
run :: R o (I (R o)) -> R o (I (R o)) -> o
run x (R f) = f x
rir :: (R o) (I (R o))
rir = R (\x -> run x x)
absurd :: a
absurd = run rir rir
-- ryan
On Wed, Jan 27, 2010 at 8:27 AM, Matthieu Sozeau
Dear Haskellers,
while trying to encode a paradox recently found in Coq if one has impredicativity and adds injectivity of type constructors [1] I stumbled on an apparent loop in the type checker when using GADTs, Rank2Types and EmptyDataDecls.
{-# OPTIONS -XGADTs -XRank2Types -XEmptyDataDecls #-}
module Impred where
The identity type
data ID a = ID a
I is from (* -> *) to *, we use a partial application of [ID] here.
data I f where I1 :: I ID
The usual reification of type equality into a term.
data Equ a b where Eqrefl :: Equ a a
The empty type
data False
This uses impredicativity: Rdef embeds a (* -> *) -> * object into R x :: *.
data R x where Rdef :: (forall a. Equ x (I a) -> a x -> False) -> R x
r_eqv1 :: forall p. R (I p) -> p (I p) -> False r_eqv1 (Rdef f) pip = f Eqrefl pip
r_eqv2 :: forall p. (p (I p) -> False) -> R (I p) r_eqv2 f = Rdef (\ eq ax -> case eq of -- Uses injectivity of type constructors Eqrefl -> f ax)
r_eqv_not_R_1 :: R (I R) -> R (I R) -> False r_eqv_not_R_1 = r_eqv1
r_eqv_not_R_2 :: (R (I R) -> False) -> R (I R) r_eqv_not_R_2 = r_eqv2
rir :: R (I R) rir = r_eqv_not_R_2 (\ rir -> r_eqv_not_R_1 rir rir)
Type checking seems to loop here with ghc-6.8.3, which is a bit strange given the simplicity of the typing problem. Maybe it triggers a constraint with something above?
-- Loops -- absurd :: False -- absurd = r_eqv_not_R_1 rir rir
[1] http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/4322/focus=...
-- Matthieu _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Ryan Ingram wrote:
The compiler doesn't loop for me with GHC6.10.4; I think GADTs still had some bugs in GHC6.8.
That said, this is pretty scary. Here's a simplified version that shows this paradox with just a single GADT and no other extensions. No use of "fix" or recursion anywhere!
{-# LANGUAGE GADTs #-} module Contr where
newtype I f = I (f ()) data R o a where R :: (a (I a) -> o) -> R o (I a)
run :: R o (I (R o)) -> R o (I (R o)) -> o run x (R f) = f x rir :: (R o) (I (R o)) rir = R (\x -> run x x)
absurd :: a absurd = run rir rir
I think that's essentially the same as this: data Fix a = Fix { unFix :: Fix a -> a } run :: Fix a -> Fix a -> a run x f = unFix f x rir :: Fix a rir = Fix (\x -> run x x) absurd :: a absurd = run rir rir Non-positive recursive occurrences in type definitions provide various ways to encode the Y-combinator in a typed lambda calculus, without the need for any recursive "let" primitive. Haskell allows such non-positive occurrences, but for strong normalisation, languages like Coq must disallow them. If you change "data" to "newtype" in the above, the GHC 6.10.4 compiler (but not GHCi) will loop. I think this is just a case of the infelicity documented here: http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html Regards, Matthew
But your example uses a recursive type; the interesting bit about this
example is that there is no recursive types or function, and yet we
can encode this loop.
-- ryan
On Wed, Jan 27, 2010 at 4:49 PM, Matthew Brecknell
Ryan Ingram wrote:
The compiler doesn't loop for me with GHC6.10.4; I think GADTs still had some bugs in GHC6.8.
That said, this is pretty scary. Here's a simplified version that shows this paradox with just a single GADT and no other extensions. No use of "fix" or recursion anywhere!
{-# LANGUAGE GADTs #-} module Contr where
newtype I f = I (f ()) data R o a where R :: (a (I a) -> o) -> R o (I a)
run :: R o (I (R o)) -> R o (I (R o)) -> o run x (R f) = f x rir :: (R o) (I (R o)) rir = R (\x -> run x x)
absurd :: a absurd = run rir rir
I think that's essentially the same as this:
data Fix a = Fix { unFix :: Fix a -> a }
run :: Fix a -> Fix a -> a run x f = unFix f x
rir :: Fix a rir = Fix (\x -> run x x)
absurd :: a absurd = run rir rir
Non-positive recursive occurrences in type definitions provide various ways to encode the Y-combinator in a typed lambda calculus, without the need for any recursive "let" primitive. Haskell allows such non-positive occurrences, but for strong normalisation, languages like Coq must disallow them.
If you change "data" to "newtype" in the above, the GHC 6.10.4 compiler (but not GHCi) will loop. I think this is just a case of the infelicity documented here:
http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html
Regards, Matthew
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Thu, 28 Jan 2010 18:32:02 -0800, Ryan Ingram
But your example uses a recursive type; the interesting bit about this example is that there is no recursive types or function, and yet we can encode this loop.
The point is that you get the Fix type by (infintely) unfolding the type definitions. -- Nicolas Pouillard http://nicolaspouillard.fr
participants (4)
-
Matthew Brecknell -
Matthieu Sozeau -
Nicolas Pouillard -
Ryan Ingram