Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- class Universe a where
- universe :: [a]
- class Universe a => Finite a where
- universeF :: [a]
- cardinality :: Tagged a Natural
- universeGeneric :: (Generic a, GUniverse (Rep a)) => [a]
- module Data.Universe.Instances.Extended
Documentation
Creating an instance of this class is a declaration that your type is
recursively enumerable (and that universe
is that enumeration). In
particular, you promise that any finite inhabitant has a finite index in
universe
, and that no inhabitant appears at two different finite indices.
Well-behaved instance should produce elements lazily.
Laws:
elem
xuniverse
-- any inhabitant has a finite index let pfx =take
nuniverse
-- any finite prefix of universe has unique elements inlength
pfx =length
(nub pfx)
Nothing
Instances
class Universe a => Finite a where #
Creating an instance of this class is a declaration that your universe
eventually ends. Minimal definition: no methods defined. By default,
universeF = universe
, but for some types (like Either
) the universeF
method may have a more intuitive ordering.
Laws:
elem
xuniverseF
-- any inhabitant has a finite indexlength
(filter
(== x)universeF
) == 1 -- should terminate (xs ->cardinality
xs ==genericLength
xs)universeF
Note:
may not hold for all types, though the laws imply that elemIndex
x universe
== elemIndex
x universeF
universe
is a permutation of universeF
.
>>>
elemIndex (Left True :: Either Bool Bool) universe
Just 2
>>>
elemIndex (Left True :: Either Bool Bool) universeF
Just 1
Nothing
Instances
universeGeneric :: (Generic a, GUniverse (Rep a)) => [a] #
>>>
data Zero deriving (Show, Generic)
>>>
universeGeneric :: [Zero]
[]
>>>
data One = One deriving (Show, Generic)
>>>
universeGeneric :: [One]
[One]
>>>
data Big = B0 Bool Bool | B1 Bool deriving (Show, Generic)
>>>
universeGeneric :: [Big]
[B0 False False,B1 False,B0 False True,B1 True,B0 True False,B0 True True]
>>>
universeGeneric :: [Maybe Ordering]
[Nothing,Just LT,Just EQ,Just GT]
>>>
take 10 (universeGeneric :: [Either Integer Integer])
[Left 0,Right 0,Left 1,Right 1,Left (-1),Right (-1),Left 2,Right 2,Left (-2),Right (-2)]
>>>
take 10 (universeGeneric :: [(Integer, Integer, Integer)])
[(0,0,0),(0,0,1),(1,0,0),(0,1,0),(1,0,1),(-1,0,0),(0,0,-1),(1,1,0),(-1,0,1),(2,0,0)]