Infinite recursion when enumerating all values of

2019-06-16 07:57发布

问题:

For another answer of mine, I wrote the following code, providing diagonally traversed Universe instances for enumerable Generics (it's slightly updated from the version there, but uses the same logic):

{-# LANGUAGE DeriveGeneric, TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts, DefaultSignatures #-}
{-# LANGUAGE UndecidableInstances, OverlappingInstances #-}

import Data.Universe
import Control.Monad.Omega
import GHC.Generics
import Control.Monad (mplus, liftM2)

class GUniverse f where
    guniverse :: Omega (f x)

instance GUniverse U1 where
    guniverse = return U1

instance (Universe c) => GUniverse (K1 i c) where
    guniverse = fmap K1 $ each (universe :: [c])        -- (1)

instance (GUniverse f) => GUniverse (M1 i c f) where
    guniverse = fmap M1 (guniverse :: Omega (f p))

instance (GUniverse f, GUniverse g) => GUniverse (f :*: g) where
    guniverse = liftM2 (:*:) ls rs
        where ls = (guniverse :: Omega (f p))
              rs = (guniverse :: Omega (g p))

instance (GUniverse f, GUniverse g) => GUniverse (f :+: g) where
    guniverse = (fmap L1 $ ls) `mplus` (fmap R1 $ rs)   -- (2)
        where ls = (guniverse :: Omega (f p))
              rs = (guniverse :: Omega (g p))

instance (Generic a, GUniverse (Rep a)) => Universe a where
    universe = runOmega $ fmap to $ (guniverse :: Omega (Rep a x))

(Omega is probably not related to the problem, but was part of the question.)

This works for most types, even recursive ones like those:

data T6 = T6' | T6 T6 deriving (Show, Generic)
data T = A | B T | C T T deriving (Show, Generic)
data Tree a = Leaf a | Branch (Tree a) (Tree a) deriving (Show, Generic, Eq)

Examples:

*Main> take 5 $ (universe :: [T6])
[T6',T6 T6',T6 (T6 T6'),T6 (T6 (T6 T6')),T6 (T6 (T6 (T6 T6')))]
*Main> take 5 $ (universe :: [T])
[A,B A,B (B A),C A A,B (B (B A))]
*Main> take 5 $ (universe :: [Tree Bool])
[Leaf False,Leaf True,Branch (Leaf False) (Leaf False),Branch (Leaf False) (Leaf True),Branch (Leaf True) (Leaf False)]

But note that above types all have their recursive constructors not at the first place! In fact (and this is the problem), the following diverges:

*Main> data T7 = T7 T7 | T7' deriving (Show, Generic)
*Main> take 5 $ (universe :: [T7])
*** Exception: <<loop>>

I first thought that maybe there's something with Omegas's evaluation order, but swapping the left and right parts in line (2) only makes T7 work, and T6 fail, which is what I'd expect as correct behavior.

My current suspicion is that the call to universe in line (1) is evaluated too early. For example, the following also diverges, while there should be exactly one value in the list, which should not even be evaluated:

*Main> data T8 = T8 T8  deriving (Show, Generic)
*Main> null $ (universe :: [T8])
*** Exception: <<loop>>

So, the only instance, T8 (T8 (...) ... ), gets evaluated inside the list, even though it is not needed! I have no idea where this effect is coming from -- is it the recursive use of its own Universe instance? But why, then, do "right recursive" types like T6 behave correctly, while "left recursive" ones (T7) don't?

Is this a strictness issue? If so, in which part of the code? My Universe instance? Generic? And how to fix it? I use GHC 7.6.3, if that matters.

回答1:

Types like T8 can't be generated this. Let's look at what the generics version of universe for T8 actually reduces to:

t8Universe :: [T8]
t8Universe = fmap T8 t8Universe

At no point is a (:) or [] produced. Without another non-recursive constructor to successfully produce there's no way to make progress. t8Universe has exactly as many elements as t8Universe has, but that's circular, and so evaluation loops.