GHC sometimes loops
February 9th, 2007 by WouterI gave a quick demo on how to make ghc loop. The trick is to encode recursion using a data type, and then write a diverging term. The compiler’s aggresive inliner then gets carried away, resulting in divergance. Here’s the code:
February 9th, 2007 at 10:23 pm
This behaviour is documented in the GHC manual: http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html
Of course, turning off inlining for apply will fix the problem. You can do that with the pragma:
{-# NOINLINE apply #-}
It would be nice if they could detect and avoid problems of this sort, though I doubt that finding a cleverly efficient solution is a terribly high priority on anyone’s list, seeing as such types only seem to occur in programs contrived to make the compiler unhappy.
The problem occurs with recursive types which occur contravariantly (i.e. as function parameters) in their own definition — detecting this directly isn’t entirely trivial due to parametric and mutually recursive types.
February 12th, 2007 at 11:57 am
Yep – I’m not the first person to run into this.
I should probably mention that I ran into this after Peter Morris talked about strictly positive families, i.e. GADTS that cannot encode recursion in this way. I was curious what this recursion encoding would look like, and was pretty startled when GHC didn’t terminate. I would expect them to limit the number of inline steps to avoid this kind of behaviour.
I don’t entirely agree that this is a completely artificial example. Imagine writing a lambda calculus interpreter using higher-order abstract syntax. If you’re not careful, you can’t write the y-combinator without your compiler diverging:
rec f = Lam (\x -> f `apply` (x `apply` x))
y = Lam (\f -> (rec f) `apply` (rec f))
Having a compiler loop is somehow wrong, even if the example is contrived.