Re: [Haskell-cafe] Non-termination of type-checking
On Thu, 28 Jan 2010 18:32:02 -0800, Ryan Ingram ryani.s...@gmail.com wrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-termination of type-checking
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
matt...@brecknell.net wrote:
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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=1405
-- Matthieu
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-termination of type-checking
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 mat...@mattam.org wrote:
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=1405
-- Matthieu
___
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
Re: [Haskell-cafe] Non-termination of type-checking
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
