Бесконечная рекурсия при перечислении всех значений универсального экземпляра

Question

Для другого ответа я написал следующий код, предоставляя по диагонали Universe экземпляры для перечислимых Generic s (он немного обновлен по сравнению с версией, но использует ту же логику):

{-# 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 вероятно не связано с проблемой, но было частью вопроса.)

Это работает для большинства типов, даже рекурсивных, таких как:

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)

Примеры:

*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)]

Но обратите внимание, что все вышеперечисленные типы имеют свои рекурсивные конструкторы не на первом месте! На самом деле (и это проблема) следующее расходится:

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

Сначала я подумал, что, может быть, есть что-то с Omegas порядок оценки, но поменялись местами левая и правая части (2) только делает T7 работа и T6 терпеть неудачу, что я и ожидал как правильное поведение.

В настоящее время я подозреваю, что universe в соответствии (1) оценивается слишком рано. Например, следующее также расходится, хотя в списке должно быть ровно одно значение, которое даже не следует оценивать:

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

Итак, единственный случай, T8 (T8 (...) ... ), оценивается внутри списка, даже если это не нужно! Я понятия не имею, откуда этот эффект - рекурсивное ли это его использование? Universe пример? Но почему же тогда "правильные рекурсивные" типы, такие как T6 вести себя корректно, в то время как "левые рекурсивные" (T7) нет?

Это проблема строгости? Если да, то в какой части кода? мой Universe пример? Generic? И как это исправить? Я использую GHC 7.6.3, если это имеет значение.

Answer 1

Типы как T8 не может быть сгенерировано это. Давайте посмотрим, к чему сводится универсальная версия юниверса для T8:

t8Universe :: [T8]
t8Universe = fmap T8 t8Universe

Ни в коем случае не создается (:) или []. Без другого нерекурсивного конструктора для успешного производства нет никакого способа добиться прогресса. t8Universe имеет столько же элементов, сколько t8Universe имеет, но это круговой, и поэтому оценки циклов.