Data.Universe.Instances.Extended

Documentation

Instances for Universe and Finite for function-like functors and the empty type.

class Universe a where

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 x universe                    -- any inhabitant has a finite index
let pfx = take n universe          -- any finite prefix of universe has unique elements
in length pfx = length (nub pfx)

Minimal complete definition

Nothing

Methods

universe :: [a]

Instances

Universe Bool

Defined in Data.Universe.Class

Methods

universe :: [Bool]

Universe Char

Defined in Data.Universe.Class

Methods

universe :: [Char]

Universe Int

Defined in Data.Universe.Class

Methods

universe :: [Int]

Universe Int8

Defined in Data.Universe.Class

Methods

universe :: [Int8]

Universe Int16

Defined in Data.Universe.Class

Methods

universe :: [Int16]

Universe Int32

Defined in Data.Universe.Class

Methods

universe :: [Int32]

Universe Int64

Defined in Data.Universe.Class

Methods

universe :: [Int64]

Universe Integer

Defined in Data.Universe.Class

Methods

universe :: [Integer]

Universe Natural

Defined in Data.Universe.Class

Methods

universe :: [Natural]

Universe Ordering

Defined in Data.Universe.Class

Methods

universe :: [Ordering]

Universe Word

Defined in Data.Universe.Class

Methods

universe :: [Word]

Universe Word8

Defined in Data.Universe.Class

Methods

universe :: [Word8]

Universe Word16

Defined in Data.Universe.Class

Methods

universe :: [Word16]

Universe Word32

Defined in Data.Universe.Class

Methods

universe :: [Word32]

Universe Word64

Defined in Data.Universe.Class

Methods

universe :: [Word64]

Universe ()

Defined in Data.Universe.Class

Methods

universe :: [()]

Universe Void

Defined in Data.Universe.Class

Methods

universe :: [Void]

Universe All

Defined in Data.Universe.Class

Methods

universe :: [All]

Universe Any

Defined in Data.Universe.Class

Methods

universe :: [Any]

Universe a => Universe [a]

Defined in Data.Universe.Class

Methods

universe :: [[a]]

Universe a => Universe (Maybe a)

Defined in Data.Universe.Class

Methods

universe :: [Maybe a]

RationalUniverse a => Universe (Ratio a)

Defined in Data.Universe.Class

Methods

universe :: [Ratio a]

(Finite a, Ord a) => Universe (Predicate a)

Defined in Data.Universe.Instances.Extended

Methods

universe :: [Predicate a]

Universe a => Universe (Min a)

Defined in Data.Universe.Class

Methods

universe :: [Min a]

Universe a => Universe (Max a)

Defined in Data.Universe.Class

Methods

universe :: [Max a]

Universe a => Universe (First a)

Defined in Data.Universe.Class

Methods

universe :: [First a]

Universe a => Universe (Last a)

Defined in Data.Universe.Class

Methods

universe :: [Last a]

Universe a => Universe (Identity a)

Defined in Data.Universe.Class

Methods

universe :: [Identity a]

Universe a => Universe (First a)

Defined in Data.Universe.Class

Methods

universe :: [First a]

Universe a => Universe (Last a)

Defined in Data.Universe.Class

Methods

universe :: [Last a]

Universe a => Universe (Dual a)

Defined in Data.Universe.Class

Methods

universe :: [Dual a]

Universe a => Universe (Sum a)

Defined in Data.Universe.Class

Methods

universe :: [Sum a]

Universe a => Universe (Product a)

Defined in Data.Universe.Class

Methods

universe :: [Product a]

Universe a => Universe (NonEmpty a)

Defined in Data.Universe.Class

Methods

universe :: [NonEmpty a]

(Ord a, Universe a) => Universe (Set a)

Defined in Data.Universe.Class

Methods

universe :: [Set a]

(Finite a, Ord a, Universe b) => Universe (a -> b)

Defined in Data.Universe.Class

Methods

universe :: [a -> b]

(Universe a, Universe b) => Universe (Either a b)

Defined in Data.Universe.Class

Methods

universe :: [Either a b]

(Universe a, Universe b) => Universe (a, b)

Defined in Data.Universe.Class

Methods

universe :: [(a, b)]

(Universe a, Finite b, Ord b) => Universe (Op a b)

Defined in Data.Universe.Instances.Extended

Methods

universe :: [Op a b]

(Representable f, Finite (Rep f), Ord (Rep f), Universe a) => Universe (Co f a)

We could do this:

instance Universe (f a) => Universe (Co f a) where universe = map Rep universe

However, since you probably only apply Rep to functors when you want to think of them as being representable, I think it makes sense to use an instance based on the representable-ness rather than the inherent universe-ness.

Please complain if you disagree!

Defined in Data.Universe.Instances.Extended

Methods

universe :: [Co f a]

Universe (Proxy a)

Defined in Data.Universe.Class

Methods

universe :: [Proxy a]

(Ord k, Finite k, Universe v) => Universe (Map k v)

Defined in Data.Universe.Class

Methods

universe :: [Map k v]

(Universe a, Universe b, Universe c) => Universe (a, b, c)

Defined in Data.Universe.Class

Methods

universe :: [(a, b, c)]

Universe a => Universe (Const a b)

Defined in Data.Universe.Class

Methods

universe :: [Const a b]

(Representable f, Finite s, Ord s, Finite (Rep f), Ord (Rep f), Universe a) => Universe (TracedT s f a)

Defined in Data.Universe.Instances.Extended

Methods

universe :: [TracedT s f a]

Universe (f a) => Universe (IdentityT f a)

Defined in Data.Universe.Class

Methods

universe :: [IdentityT f a]

Universe a => Universe (Tagged b a)

Defined in Data.Universe.Class

Methods

universe :: [Tagged b a]

(Universe a, Universe b, Universe c, Universe d) => Universe (a, b, c, d)

Defined in Data.Universe.Class

Methods

universe :: [(a, b, c, d)]

(Universe (f a), Universe (g a)) => Universe (Product f g a)

Defined in Data.Universe.Class

Methods

universe :: [Product f g a]

(Universe (f a), Universe (g a)) => Universe (Sum f g a)

Defined in Data.Universe.Class

Methods

universe :: [Sum f g a]

(Finite e, Ord e, Universe (m a)) => Universe (ReaderT e m a)

Defined in Data.Universe.Class

Methods

universe :: [ReaderT e m a]

(Universe a, Universe b, Universe c, Universe d, Universe e) => Universe (a, b, c, d, e)

Defined in Data.Universe.Class

Methods

universe :: [(a, b, c, d, e)]

Universe (f (g a)) => Universe (Compose f g a)

Defined in Data.Universe.Class

Methods

universe :: [Compose f g a]

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 x universeF                       -- any inhabitant has a finite index
length (filter (== x) universeF) == 1  -- should terminate
(xs -> cardinality xs == genericLength xs) universeF

Note: elemIndex x universe == elemIndex x universeF may not hold for all types, though the laws imply that universe is a permutation of universeF.

>>> elemIndex (Left True :: Either Bool Bool) universe
Just 2

>>> elemIndex (Left True :: Either Bool Bool) universeF
Just 1

Minimal complete definition

Nothing

Methods

universeF :: [a]

cardinality :: Tagged a Natural

Instances

Finite Bool

Defined in Data.Universe.Class

Methods

universeF :: [Bool]

cardinality :: Tagged Bool Natural

Finite Char

Defined in Data.Universe.Class

Methods

universeF :: [Char]

cardinality :: Tagged Char Natural

Finite Int

Defined in Data.Universe.Class

Methods

universeF :: [Int]

cardinality :: Tagged Int Natural

Finite Int8

Defined in Data.Universe.Class

Methods

universeF :: [Int8]

cardinality :: Tagged Int8 Natural

Finite Int16

Defined in Data.Universe.Class

Methods

universeF :: [Int16]

cardinality :: Tagged Int16 Natural

Finite Int32

Defined in Data.Universe.Class

Methods

universeF :: [Int32]

cardinality :: Tagged Int32 Natural

Finite Int64

Defined in Data.Universe.Class

Methods

universeF :: [Int64]

cardinality :: Tagged Int64 Natural

Finite Ordering

Defined in Data.Universe.Class

Methods

universeF :: [Ordering]

cardinality :: Tagged Ordering Natural

Finite Word

Defined in Data.Universe.Class

Methods

universeF :: [Word]

cardinality :: Tagged Word Natural

Finite Word8

Defined in Data.Universe.Class

Methods

universeF :: [Word8]

cardinality :: Tagged Word8 Natural

Finite Word16

Defined in Data.Universe.Class

Methods

universeF :: [Word16]

cardinality :: Tagged Word16 Natural

Finite Word32

Defined in Data.Universe.Class

Methods

universeF :: [Word32]

cardinality :: Tagged Word32 Natural

Finite Word64

Defined in Data.Universe.Class

Methods

universeF :: [Word64]

cardinality :: Tagged Word64 Natural

Finite ()

Defined in Data.Universe.Class

Methods

universeF :: [()]

cardinality :: Tagged () Natural

Finite Void

Defined in Data.Universe.Class

Methods

universeF :: [Void]

cardinality :: Tagged Void Natural

Finite All

Defined in Data.Universe.Class

Methods

universeF :: [All]

cardinality :: Tagged All Natural

Finite Any

Defined in Data.Universe.Class

Methods

universeF :: [Any]

cardinality :: Tagged Any Natural

Finite a => Finite (Maybe a)

Defined in Data.Universe.Class

Methods

universeF :: [Maybe a]

cardinality :: Tagged (Maybe a) Natural

(Finite a, Ord a) => Finite (Predicate a)

>>> mapM_ print (universe :: [Predicate Ordering])
Predicate {getPredicate = [(LT,False),(EQ,False),(GT,False)]}
Predicate {getPredicate = [(LT,True),(EQ,False),(GT,False)]}
Predicate {getPredicate = [(LT,False),(EQ,True),(GT,False)]}
Predicate {getPredicate = [(LT,True),(EQ,True),(GT,False)]}
Predicate {getPredicate = [(LT,False),(EQ,False),(GT,True)]}
Predicate {getPredicate = [(LT,True),(EQ,False),(GT,True)]}
Predicate {getPredicate = [(LT,False),(EQ,True),(GT,True)]}
Predicate {getPredicate = [(LT,True),(EQ,True),(GT,True)]}

Beware, function type universes are large...

>>> cardinality :: Tagged (Predicate Int8) Natural
Tagged 115792089237316195423570985008687907853269984665640564039457584007913129639936

... but thanks to laziness, you can expect at least few:

>>> let Predicate f : _ = universe :: [Predicate Int8]
>>> f 0
False

Defined in Data.Universe.Instances.Extended

Methods

universeF :: [Predicate a]

cardinality :: Tagged (Predicate a) Natural

Finite a => Finite (Min a)

Defined in Data.Universe.Class

Methods

universeF :: [Min a]

cardinality :: Tagged (Min a) Natural

Finite a => Finite (Max a)

Defined in Data.Universe.Class

Methods

universeF :: [Max a]

cardinality :: Tagged (Max a) Natural

Finite a => Finite (First a)

Defined in Data.Universe.Class

Methods

universeF :: [First a]

cardinality :: Tagged (First a) Natural

Finite a => Finite (Last a)

Defined in Data.Universe.Class

Methods

universeF :: [Last a]

cardinality :: Tagged (Last a) Natural

Finite a => Finite (Identity a)

Defined in Data.Universe.Class

Methods

universeF :: [Identity a]

cardinality :: Tagged (Identity a) Natural

Finite a => Finite (First a)

Defined in Data.Universe.Class

Methods

universeF :: [First a]

cardinality :: Tagged (First a) Natural

Finite a => Finite (Last a)

Defined in Data.Universe.Class

Methods

universeF :: [Last a]

cardinality :: Tagged (Last a) Natural

Finite a => Finite (Dual a)

Defined in Data.Universe.Class

Methods

universeF :: [Dual a]

cardinality :: Tagged (Dual a) Natural

Finite a => Finite (Sum a)

Defined in Data.Universe.Class

Methods

universeF :: [Sum a]

cardinality :: Tagged (Sum a) Natural

Finite a => Finite (Product a)

Defined in Data.Universe.Class

Methods

universeF :: [Product a]

cardinality :: Tagged (Product a) Natural

(Ord a, Finite a) => Finite (Set a)

Defined in Data.Universe.Class

Methods

universeF :: [Set a]

cardinality :: Tagged (Set a) Natural

(Ord a, Finite a, Finite b) => Finite (a -> b)

Defined in Data.Universe.Class

Methods

universeF :: [a -> b]

cardinality :: Tagged (a -> b) Natural

(Finite a, Finite b) => Finite (Either a b)

Defined in Data.Universe.Class

Methods

universeF :: [Either a b]

cardinality :: Tagged (Either a b) Natural

(Finite a, Finite b) => Finite (a, b)

Defined in Data.Universe.Class

Methods

universeF :: [(a, b)]

cardinality :: Tagged (a, b) Natural

(Finite a, Finite b, Ord b) => Finite (Op a b)

Defined in Data.Universe.Instances.Extended

Methods

universeF :: [Op a b]

cardinality :: Tagged (Op a b) Natural

(Representable f, Finite (Rep f), Ord (Rep f), Finite a) => Finite (Co f a)

Defined in Data.Universe.Instances.Extended

Methods

universeF :: [Co f a]

cardinality :: Tagged (Co f a) Natural

Finite (Proxy a)

Defined in Data.Universe.Class

Methods

universeF :: [Proxy a]

cardinality :: Tagged (Proxy a) Natural

(Ord k, Finite k, Finite v) => Finite (Map k v)

Defined in Data.Universe.Class

Methods

universeF :: [Map k v]

cardinality :: Tagged (Map k v) Natural

(Finite a, Finite b, Finite c) => Finite (a, b, c)

Defined in Data.Universe.Class

Methods

universeF :: [(a, b, c)]

cardinality :: Tagged (a, b, c) Natural

Finite a => Finite (Const a b)

Defined in Data.Universe.Class

Methods

universeF :: [Const a b]

cardinality :: Tagged (Const a b) Natural

(Representable f, Finite s, Ord s, Finite (Rep f), Ord (Rep f), Finite a) => Finite (TracedT s f a)

Defined in Data.Universe.Instances.Extended

Methods

universeF :: [TracedT s f a]

cardinality :: Tagged (TracedT s f a) Natural

Finite (f a) => Finite (IdentityT f a)

Defined in Data.Universe.Class

Methods

universeF :: [IdentityT f a]

cardinality :: Tagged (IdentityT f a) Natural

Finite a => Finite (Tagged b a)

Defined in Data.Universe.Class

Methods

universeF :: [Tagged b a]

cardinality :: Tagged (Tagged b a) Natural

(Finite a, Finite b, Finite c, Finite d) => Finite (a, b, c, d)

Defined in Data.Universe.Class

Methods

universeF :: [(a, b, c, d)]

cardinality :: Tagged (a, b, c, d) Natural

(Finite (f a), Finite (g a)) => Finite (Product f g a)

Defined in Data.Universe.Class

Methods

universeF :: [Product f g a]

cardinality :: Tagged (Product f g a) Natural

(Finite (f a), Finite (g a)) => Finite (Sum f g a)

Defined in Data.Universe.Class

Methods

universeF :: [Sum f g a]

cardinality :: Tagged (Sum f g a) Natural

(Finite e, Ord e, Finite (m a)) => Finite (ReaderT e m a)

Defined in Data.Universe.Class

Methods

universeF :: [ReaderT e m a]

cardinality :: Tagged (ReaderT e m a) Natural

(Finite a, Finite b, Finite c, Finite d, Finite e) => Finite (a, b, c, d, e)

Defined in Data.Universe.Class

Methods

universeF :: [(a, b, c, d, e)]

cardinality :: Tagged (a, b, c, d, e) Natural

Finite (f (g a)) => Finite (Compose f g a)

Defined in Data.Universe.Class

Methods

universeF :: [Compose f g a]

cardinality :: Tagged (Compose f g a) Natural

Orphan instances

(Finite a, Ord a) => Universe (Predicate a)

Methods

universe :: [Predicate a]

(Finite a, Ord a) => Finite (Predicate a)

>>> mapM_ print (universe :: [Predicate Ordering])
Predicate {getPredicate = [(LT,False),(EQ,False),(GT,False)]}
Predicate {getPredicate = [(LT,True),(EQ,False),(GT,False)]}
Predicate {getPredicate = [(LT,False),(EQ,True),(GT,False)]}
Predicate {getPredicate = [(LT,True),(EQ,True),(GT,False)]}
Predicate {getPredicate = [(LT,False),(EQ,False),(GT,True)]}
Predicate {getPredicate = [(LT,True),(EQ,False),(GT,True)]}
Predicate {getPredicate = [(LT,False),(EQ,True),(GT,True)]}
Predicate {getPredicate = [(LT,True),(EQ,True),(GT,True)]}

Beware, function type universes are large...

>>> cardinality :: Tagged (Predicate Int8) Natural
Tagged 115792089237316195423570985008687907853269984665640564039457584007913129639936

... but thanks to laziness, you can expect at least few:

>>> let Predicate f : _ = universe :: [Predicate Int8]
>>> f 0
False

Methods

universeF :: [Predicate a]

cardinality :: Tagged (Predicate a) Natural

(Universe a, Finite b, Ord b) => Universe (Op a b)

Methods

universe :: [Op a b]

(Representable f, Finite (Rep f), Ord (Rep f), Universe a) => Universe (Co f a)

We could do this:

instance Universe (f a) => Universe (Co f a) where universe = map Rep universe

However, since you probably only apply Rep to functors when you want to think of them as being representable, I think it makes sense to use an instance based on the representable-ness rather than the inherent universe-ness.

Please complain if you disagree!

Methods

universe :: [Co f a]

(Finite a, Finite b, Ord b) => Finite (Op a b)

Methods

universeF :: [Op a b]

cardinality :: Tagged (Op a b) Natural

(Representable f, Finite (Rep f), Ord (Rep f), Finite a) => Finite (Co f a)

Methods

universeF :: [Co f a]

cardinality :: Tagged (Co f a) Natural

(Representable f, Finite s, Ord s, Finite (Rep f), Ord (Rep f), Universe a) => Universe (TracedT s f a)

Methods

universe :: [TracedT s f a]

(Representable f, Finite s, Ord s, Finite (Rep f), Ord (Rep f), Finite a) => Finite (TracedT s f a)

Methods

universeF :: [TracedT s f a]

cardinality :: Tagged (TracedT s f a) Natural