GHC sometimes loops

February 9th, 2007 by Wouter

I 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:

>data Evil = Evil (Evil -> Evil)

>apply :: Evil -> Evil -> Evil
>apply (Evil f) x = f x

>delta :: Evil
>delta = Evil (\x -> x `apply` x)

>omega :: Evil
>omega = delta `apply` delta

2 Responses to “GHC sometimes loops”

  1. Cale Gibbard Says:

    This behaviour is documented in the GHC manual:

    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.

  2. Wouter Says:

    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.

Leave a Reply