I finally found the time to write a generic version. It uses the Universe
typeclass, which represents recursively enumerabley types. Here it is:
{-# LANGUAGE DeriveGeneric, TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances, OverlappingInstances #-}
import Data.Universe
import Control.Monad.Omega
import GHC.Generics
import Control.Monad (mplus, liftM2)
class GUniverse f where
guniverse :: [f a]
instance GUniverse U1 where
guniverse = [U1]
instance (Universe c) => GUniverse (K1 i c) where
guniverse = fmap K1 (universe :: [c])
instance (GUniverse f) => GUniverse (M1 i c f) where
guniverse = fmap M1 (guniverse :: [f p])
instance (GUniverse f, GUniverse g) => GUniverse (f :*: g) where
guniverse = runOmega $ liftM2 (:*:) ls rs
where ls = each (guniverse :: [f p])
rs = each (guniverse :: [g p])
instance (GUniverse f, GUniverse g) => GUniverse (f :+: g) where
guniverse = runOmega $ (fmap L1 $ ls) `mplus` (fmap R1 $ rs)
where ls = each (guniverse :: [f p])
rs = each (guniverse :: [g p])
instance (Generic a, GUniverse (Rep a)) => Universe a where
universe = fmap to $ (guniverse :: [Rep a x])
data T = A | B T | C T T deriving (Show, Generic)
data Tree a = Leaf a | Branch (Tree a) (Tree a) deriving (Show, Generic)
I couldn't find a way to remove UndecidableInstances
, but that should be of no greater concern. OverlappingInstances
is only required to override predefined Universe
instances, like Either
's. Now some nice outputs:
*Main> take 10 $ (universe :: [T])
[A,B A,B (B A),C A A,B (B (B A)),C A (B A),B (C A A),C (B A) A,B (B (B (B A))),C A (B (B A))]
*Main> take 20 $ (universe :: [Either Int Char])
[Left (-9223372036854775808),Right '\NUL',Left (-9223372036854775807),Right '\SOH',Left (-9223372036854775806),Right '\STX',Left (-9223372036854775805),Right '\ETX',Left (-9223372036854775804),Right '\EOT',Left (-9223372036854775803),Right '\ENQ',Left (-9223372036854775802),Right '\ACK',Left (-9223372036854775801),Right '\a',Left (-9223372036854775800),Right '\b',Left (-9223372036854775799),Right '\t']
*Main> take 10 $ (universe :: [Tree Bool])
[Leaf False,Leaf True,Branch (Leaf False) (Leaf False),Branch (Leaf False) (Leaf True),Branch (Leaf True) (Leaf False),Branch (Leaf False) (Branch (Leaf False) (Leaf False)),Branch (Leaf True) (Leaf True),Branch (Branch (Leaf False) (Leaf False)) (Leaf False),Branch (Leaf False) (Branch (Leaf False) (Leaf True)),Branch (Leaf True) (Branch (Leaf False) (Leaf False))]
I'm not exactly sure what happens in the branching order of mplus
, but I think it should all work out if Omega
is correctly implemented, which I strongly believe.
But wait! The above implementation is not yet bug-free; it diverges on "left recursive" types, like this:
data T3 = T3 T3 | T3' deriving (Show, Generic)
while this works:
data T6 = T6' | T6 T6 deriving (Show, Generic)
I'll see if I can fix that. EDIT: At some time, the solution of this problem might be found in this question.