
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.]