an evil type hangs GHC

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

an evil type hangs GHC

Petr Pudlak (Debian)
Hi, I was playing with the following example I found in D.A.Turner's
paper Total Functional Programming:

> data Bad a = C (Bad a -> a)
>
> bad1 :: Bad a -> a
> bad1 b@(C f) = f b
>
> bad2 :: a
> bad2 = bad1 (C bad1)

To my surprise, instead of creating a bottom valued function (an
infinite loop), I managed to send the GHC compiler (ver. 6.12.1) to an
infinite loop. Could anybody suggest an explanation? Is this a GHC bug?
Or is this "Bad" data type so evil that type checking fails?

     Thanks,
     Petr

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (501 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: an evil type hangs GHC

Petr Pudlak (Debian)
On Fri, Nov 12, 2010 at 07:52:53PM +0100, Petr Pudlak wrote:

>Hi, I was playing with the following example I found in D.A.Turner's
>paper Total Functional Programming:
>
>>data Bad a = C (Bad a -> a)
>>
>>bad1 :: Bad a -> a
>>bad1 b@(C f) = f b
>>
>>bad2 :: a
>>bad2 = bad1 (C bad1)
>
>To my surprise, instead of creating a bottom valued function (an
>infinite loop), I managed to send the GHC compiler (ver. 6.12.1) to
>an infinite loop. Could anybody suggest an explanation? Is this a GHC
>bug? Or is this "Bad" data type so evil that type checking fails?
>
>    Thanks,
>    Petr
PS: The following code compiles, the difference is just in modifying
"bad2" to include an argument:

> data Bad a = C (Bad a -> a)
>
> bad1 :: Bad a -> a
> bad1 b@(C f) = f b
>
> bad2 :: (a -> a) -> a
> bad2 f = bad1 (C $ f . bad1)

[BTW, "bad2" has the type of the Y combinator and indeed works as
expected:

> factorial :: (Int -> Int) -> Int -> Int
> factorial _ 0 = 1
> factorial r n = n * (r (n-1))
>
> main :: IO ()
> main = print $ map (bad2 factorial) [1..10]

... so one can get general recursion just by crafting such a strange
data type.]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (501 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: an evil type hangs GHC

roconnor
See <http://www.haskell.org/pipermail/haskell/2006-September/018497.html>

On Fri, 12 Nov 2010, Petr Pudlak wrote:

> On Fri, Nov 12, 2010 at 07:52:53PM +0100, Petr Pudlak wrote:
>> Hi, I was playing with the following example I found in D.A.Turner's paper
>> Total Functional Programming:
>>
>>> data Bad a = C (Bad a -> a)
>>>
>>> bad1 :: Bad a -> a
>>> bad1 b@(C f) = f b
>>>
>>> bad2 :: a
>>> bad2 = bad1 (C bad1)
>>
>> To my surprise, instead of creating a bottom valued function (an infinite
>> loop), I managed to send the GHC compiler (ver. 6.12.1) to an infinite
>> loop. Could anybody suggest an explanation? Is this a GHC bug? Or is this
>> "Bad" data type so evil that type checking fails?
>>
>>    Thanks,
>>    Petr
>
> PS: The following code compiles, the difference is just in modifying "bad2"
> to include an argument:
>
>> data Bad a = C (Bad a -> a)
>>
>> bad1 :: Bad a -> a
>> bad1 b@(C f) = f b
>>
>> bad2 :: (a -> a) -> a
>> bad2 f = bad1 (C $ f . bad1)
>
> [BTW, "bad2" has the type of the Y combinator and indeed works as expected:
>
>> factorial :: (Int -> Int) -> Int -> Int
>> factorial _ 0 = 1
>> factorial r n = n * (r (n-1))
>>
>> main :: IO ()
>> main = print $ map (bad2 factorial) [1..10]
>
> ... so one can get general recursion just by crafting such a strange data
> type.]
>

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: an evil type hangs GHC

Ryan Ingram
In reply to this post by Petr Pudlak (Debian)
>From http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/bugs.html#bugs-ghc:

GHC's inliner can be persuaded into non-termination using the standard
way to encode recursion via a data type:

  data U = MkU (U -> Bool)

  russel :: U -> Bool
  russel u@(MkU p) = not $ p u

  x :: Bool
  x = russel (MkU russel)


On Fri, Nov 12, 2010 at 10:52 AM, Petr Pudlak <[hidden email]> wrote:

> Hi, I was playing with the following example I found in D.A.Turner's paper
> Total Functional Programming:
>
>> data Bad a = C (Bad a -> a)
>>
>> bad1 :: Bad a -> a
>> bad1 b@(C f) = f b
>>
>> bad2 :: a
>> bad2 = bad1 (C bad1)
>
> To my surprise, instead of creating a bottom valued function (an infinite
> loop), I managed to send the GHC compiler (ver. 6.12.1) to an infinite loop.
> Could anybody suggest an explanation? Is this a GHC bug? Or is this "Bad"
> data type so evil that type checking fails?
>
>    Thanks,
>    Petr
>
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.10 (GNU/Linux)
>
> iQEcBAEBAgAGBQJM3Y0FAAoJEC5dcKNjBzhn68cH/3NsoUWOheGXsjZqpYj5yp5F
> IvN7NabyrAf3nxHG5uvIRqS0U33t0wZj3xSetnzDFW6wAjVtaDR4Jo7jB2/xXhLb
> g+vN9pcyZXH/r6HPb0ozRMHva4rS6K1S5T9u0kHI8jF9oeml4/lJQDOj2oouFfn2
> yxsW8FKSfYQaDfudI2Bap3mCl8xeKaABwWIcc+4LUU0r2nmpHxBlqet9yOTBAa57
> RkQrMmpt11bEVs/OUBZ2uIbd8iRD51eYTPyMHqy14a1FaRvkAvYinXQPSbg2vYcP
> YEH2llj/hsi7oxK4LVSj85nk0Ss59qFasYdWEPmr3zLzlRSjSI9kIlM3MqTjil4=
> =R7yy
> -----END PGP SIGNATURE-----
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: an evil type hangs GHC

wren ng thornton
On 11/12/10 4:53 PM, Ryan Ingram wrote:
>> From http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/bugs.html#bugs-ghc:
>
> GHC's inliner can be persuaded into non-termination using the standard
> way to encode recursion via a data type:

More specifically, since your bad2 does not look recursive, the inliner
will get inline happy and apply the definition of bad1, but then it'll
see a constant case match that it can reduce statically, and <loop>


{ okay, let's start with bad1 }

     bad1 b@(C f) = f b

{ mmm, tasty tasty sugar }

     bad1 = \b -> case b of C f -> f b

{ ha, dare you to optimize that further }

{ okay, now let's co compile bad2 }

     bad2 = bad1 (C bad1)

{ oh look, it's nonrecursive so let's start inlining }

     bad2 = (\b -> case b of C f -> f b) (C bad1)

{ oh look, an application we can evaluate statically }

     bad2 = let b = (C bad1) in case b of C f -> f b

{ meh, let's ignore sharing for now }

     bad2 = case (C bad1) of C f -> f (C bad1)

{ oh look, a case analysis we can evaluate statically }

     bad2 = let f = bad1 in f (C bad1)

{ oh look, f is only used once so we can substitute the let }
{ and if we didn't ignore sharing before, then we'd see that b is only
used once now, so we could substitute that let too }

     bad2 = bad1 (C bad1)

{ oh look, it's nonrecursive so let's start inlining }

--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe