{-# LANGUAGE CPP, BangPatterns, TypeFamilies, ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
#ifdef DEFAULT_SIGNATURES
{-# LANGUAGE DefaultSignatures #-}
#endif
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >=704
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >=702
{-# LANGUAGE Trustworthy #-}
#endif
-- | Bottoms are ignored for this entire module:
-- only fully-defined inhabitants are considered inhabitants.
module Data.Universe.Class
  ( Universe(..)
  , Finite(..)
  ) where

import Data.Universe.Helpers

import Control.Applicative (Const (..))
import Control.Monad (liftM2, liftM3, liftM4, liftM5)
import Control.Monad.Trans.Identity (IdentityT (..))
import Control.Monad.Trans.Reader (ReaderT (..))
import Data.Functor.Compose (Compose (..))
import Data.Functor.Identity (Identity (..))
import Data.Functor.Product (Product (..))
import Data.Functor.Sum (Sum (..))
import Data.Int (Int, Int8, Int16, Int32, Int64)
import Data.List (genericLength)
import Data.List.NonEmpty (NonEmpty (..))
import Data.Map ((!), fromList)
import Data.Proxy (Proxy (..))
import Data.Ratio (Ratio, numerator, denominator, (%))
import Data.Tagged (Tagged (..), retag)
import Data.Void (Void)
import Data.Word  (Word, Word8, Word16, Word32, Word64)
import GHC.Real (Ratio (..))
import Numeric.Natural (Natural)

import qualified Data.Monoid as Mon
import qualified Data.Semigroup as Semi
import qualified Data.Set as Set
import qualified Data.Map as Map

-- $setup
-- >>> import Data.List
-- >>> import Data.Universe.Helpers
--
-- -- Show (a -> b) instance (in universe-reverse-instances, but cannot depend on it here).
-- >>> instance (Finite a, Show a, Show b) => Show (a -> b) where showsPrec n f = showsPrec n [(a, f a) | a <- universeF]

-- | 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)
-- @
class Universe a where
  universe :: [a]
#ifdef DEFAULT_SIGNATURES
  default universe :: (Enum a, Bounded a) => [a]
  universe = [a]
forall a. (Bounded a, Enum a) => [a]
universeDef
#endif

-- | 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
--
class Universe a => Finite a where
  universeF :: [a]
  universeF = [a]
forall a. Universe a => [a]
universe

  cardinality :: Tagged a Natural
  cardinality = Natural -> Tagged a Natural
forall k (s :: k) b. b -> Tagged s b
Tagged ([a] -> Natural
forall i a. Num i => [a] -> i
genericLength ([a]
forall a. Finite a => [a]
universeF :: [a]))

-------------------------------------------------------------------------------
-- Base
-------------------------------------------------------------------------------

instance Universe ()       where universe :: [()]
universe = [()]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Bool     where universe :: [Bool]
universe = [Bool]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Char     where universe :: [Char]
universe = [Char]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Ordering where universe :: [Ordering]
universe = [Ordering]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Integer  where universe :: [Integer]
universe = [Integer
0, -Integer
1..] [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
+++ [Integer
1..]
instance Universe Natural  where universe :: [Natural]
universe = [Natural
0..]
instance Universe Int      where universe :: [Int]
universe = [Int]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Int8     where universe :: [Int8]
universe = [Int8]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Int16    where universe :: [Int16]
universe = [Int16]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Int32    where universe :: [Int32]
universe = [Int32]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Int64    where universe :: [Int64]
universe = [Int64]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Word     where universe :: [Word]
universe = [Word]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Word8    where universe :: [Word8]
universe = [Word8]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Word16   where universe :: [Word16]
universe = [Word16]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Word32   where universe :: [Word32]
universe = [Word32]
forall a. (Bounded a, Enum a) => [a]
universeDef
instance Universe Word64   where universe :: [Word64]
universe = [Word64]
forall a. (Bounded a, Enum a) => [a]
universeDef

instance (Universe a, Universe b) => Universe (Either a b) where universe :: [Either a b]
universe = (a -> Either a b) -> [a] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Either a b
forall a b. a -> Either a b
Left [a]
forall a. Universe a => [a]
universe [Either a b] -> [Either a b] -> [Either a b]
forall a. [a] -> [a] -> [a]
+++ (b -> Either a b) -> [b] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map b -> Either a b
forall a b. b -> Either a b
Right [b]
forall a. Universe a => [a]
universe
instance  Universe a              => Universe (Maybe  a  ) where universe :: [Maybe a]
universe = Maybe a
forall a. Maybe a
Nothing Maybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
: (a -> Maybe a) -> [a] -> [Maybe a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Maybe a
forall a. a -> Maybe a
Just [a]
forall a. Universe a => [a]
universe

instance (Universe a, Universe b) => Universe (a, b) where universe :: [(a, b)]
universe = [a]
forall a. Universe a => [a]
universe [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [b]
forall a. Universe a => [a]
universe
instance (Universe a, Universe b, Universe c) => Universe (a, b, c) where universe :: [(a, b, c)]
universe = [(a
a,b
b,c
c) | ((a
a,b
b),c
c) <- [a]
forall a. Universe a => [a]
universe [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [b]
forall a. Universe a => [a]
universe [(a, b)] -> [c] -> [((a, b), c)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [c]
forall a. Universe a => [a]
universe]
instance (Universe a, Universe b, Universe c, Universe d) => Universe (a, b, c, d) where universe :: [(a, b, c, d)]
universe = [(a
a,b
b,c
c,d
d) | (((a
a,b
b),c
c),d
d) <- [a]
forall a. Universe a => [a]
universe [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [b]
forall a. Universe a => [a]
universe [(a, b)] -> [c] -> [((a, b), c)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [c]
forall a. Universe a => [a]
universe [((a, b), c)] -> [d] -> [(((a, b), c), d)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [d]
forall a. Universe a => [a]
universe]
instance (Universe a, Universe b, Universe c, Universe d, Universe e) => Universe (a, b, c, d, e) where universe :: [(a, b, c, d, e)]
universe = [(a
a,b
b,c
c,d
d,e
e) | ((((a
a,b
b),c
c),d
d),e
e) <- [a]
forall a. Universe a => [a]
universe [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [b]
forall a. Universe a => [a]
universe [(a, b)] -> [c] -> [((a, b), c)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [c]
forall a. Universe a => [a]
universe [((a, b), c)] -> [d] -> [(((a, b), c), d)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [d]
forall a. Universe a => [a]
universe [(((a, b), c), d)] -> [e] -> [((((a, b), c), d), e)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [e]
forall a. Universe a => [a]
universe]

instance Universe a => Universe [a] where
  universe :: [[a]]
universe = [[[a]]] -> [[a]]
forall a. [[a]] -> [a]
diagonal ([[[a]]] -> [[a]]) -> [[[a]]] -> [[a]]
forall a b. (a -> b) -> a -> b
$ [[]] [[a]] -> [[[a]]] -> [[[a]]]
forall a. a -> [a] -> [a]
: [[a
ha -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
t | [a]
t <- [[a]]
forall a. Universe a => [a]
universe] | a
h <- [a]
forall a. Universe a => [a]
universe]

instance Universe a => Universe (NonEmpty a) where
  universe :: [NonEmpty a]
universe = [[NonEmpty a]] -> [NonEmpty a]
forall a. [[a]] -> [a]
diagonal [[a
h a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
t | [a]
t <- [[a]]
forall a. Universe a => [a]
universe] | a
h <- [a]
forall a. Universe a => [a]
universe]

instance Universe Mon.All where universe :: [All]
universe = (Bool -> All) -> [Bool] -> [All]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> All
Mon.All [Bool]
forall a. Universe a => [a]
universe
instance Universe Mon.Any where universe :: [Any]
universe = (Bool -> Any) -> [Bool] -> [Any]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> Any
Mon.Any [Bool]
forall a. Universe a => [a]
universe
instance Universe a => Universe (Mon.Sum     a) where universe :: [Sum a]
universe = (a -> Sum a) -> [a] -> [Sum a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Sum a
forall a. a -> Sum a
Mon.Sum     [a]
forall a. Universe a => [a]
universe
instance Universe a => Universe (Mon.Product a) where universe :: [Product a]
universe = (a -> Product a) -> [a] -> [Product a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Product a
forall a. a -> Product a
Mon.Product [a]
forall a. Universe a => [a]
universe
instance Universe a => Universe (Mon.Dual    a) where universe :: [Dual a]
universe = (a -> Dual a) -> [a] -> [Dual a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Dual a
forall a. a -> Dual a
Mon.Dual    [a]
forall a. Universe a => [a]
universe
instance Universe a => Universe (Mon.First   a) where universe :: [First a]
universe = (Maybe a -> First a) -> [Maybe a] -> [First a]
forall a b. (a -> b) -> [a] -> [b]
map Maybe a -> First a
forall a. Maybe a -> First a
Mon.First   [Maybe a]
forall a. Universe a => [a]
universe
instance Universe a => Universe (Mon.Last    a) where universe :: [Last a]
universe = (Maybe a -> Last a) -> [Maybe a] -> [Last a]
forall a b. (a -> b) -> [a] -> [b]
map Maybe a -> Last a
forall a. Maybe a -> Last a
Mon.Last    [Maybe a]
forall a. Universe a => [a]
universe

-------------------------------------------------------------------------------
-- Semi
-------------------------------------------------------------------------------

instance Universe a => Universe (Semi.Max   a) where universe :: [Max a]
universe = (a -> Max a) -> [a] -> [Max a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Max a
forall a. a -> Max a
Semi.Max   [a]
forall a. Universe a => [a]
universe
instance Universe a => Universe (Semi.Min   a) where universe :: [Min a]
universe = (a -> Min a) -> [a] -> [Min a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Min a
forall a. a -> Min a
Semi.Min   [a]
forall a. Universe a => [a]
universe
instance Universe a => Universe (Semi.First a) where universe :: [First a]
universe = (a -> First a) -> [a] -> [First a]
forall a b. (a -> b) -> [a] -> [b]
map a -> First a
forall a. a -> First a
Semi.First [a]
forall a. Universe a => [a]
universe
instance Universe a => Universe (Semi.Last  a) where universe :: [Last a]
universe = (a -> Last a) -> [a] -> [Last a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Last a
forall a. a -> Last a
Semi.Last  [a]
forall a. Universe a => [a]
universe

-------------------------------------------------------------------------------
-- Rational
-------------------------------------------------------------------------------

-- see http://mathlesstraveled.com/2008/01/07/recounting-the-rationals-part-ii-fractions-grow-on-trees/
--
-- also, Brent Yorgey writes:
--
-- positiveRationals2 :: [Ratio Integer]
-- positiveRationals2 = iterate' next 1
--   where
--     next x = let (n,y) = properFraction x in recip (fromInteger n + 1 - y)
--     iterate' f x = let x' = f x in x' `seq` (x : iterate' f x')
--
-- But this turns out to be substantially slower.
--
-- We used to use
--
--    positiveRationals =
--      1 : map lChild positiveRationals +++ map rChild positiveRationals
--
-- where lChild and rChild produced the left and right child of each fraction,
-- respectively. Aside from building unnecessary thunks (thanks to the lazy
-- map), this had the problem of calculating each sum at least four times:
-- once for a denominator, a second time for the following numerator, and then two
-- more times on the other side of the Calkin-Wilf tree. That doesn't
-- sound too bad, since in practice the integers will be small. But taking each
-- sum allocates a constructor to wrap the result, and that's not
-- free. We can avoid the problem with very little additional effort by
-- interleaving manually. Negative rationals, unfortunately, don't get the
-- full benefit of sharing here, but we can still share their denominators.

infixr 5 :<
data Stream a = !a :< Stream a

-- All the rational numbers on the left side of the Calkin-Wilf tree,
-- in breadth-first order.
leftSideStream :: Integral a => Stream (Ratio a)
leftSideStream :: Stream (Ratio a)
leftSideStream = a
1 a -> a -> Ratio a
forall a. a -> a -> Ratio a
:% a
2 Ratio a -> Stream (Ratio a) -> Stream (Ratio a)
forall a. a -> Stream a -> Stream a
:< Stream (Ratio a) -> Stream (Ratio a)
forall a. Num a => Stream (Ratio a) -> Stream (Ratio a)
go Stream (Ratio a)
forall a. Integral a => Stream (Ratio a)
leftSideStream
  where
      go :: Stream (Ratio a) -> Stream (Ratio a)
go (Ratio a
x :< Stream (Ratio a)
xs) = Ratio a
lChild Ratio a -> Stream (Ratio a) -> Stream (Ratio a)
forall a. a -> Stream a -> Stream a
:< Ratio a
rChild Ratio a -> Stream (Ratio a) -> Stream (Ratio a)
forall a. a -> Stream a -> Stream a
:< Stream (Ratio a) -> Stream (Ratio a)
go Stream (Ratio a)
xs
        where
          nd :: a
nd = Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
x a -> a -> a
forall a. Num a => a -> a -> a
+ Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
x
          !lChild :: Ratio a
lChild = Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
x a -> a -> Ratio a
forall a. a -> a -> Ratio a
:% a
nd
          !rChild :: Ratio a
rChild = a
nd a -> a -> Ratio a
forall a. a -> a -> Ratio a
:% Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
x

instance RationalUniverse a => Universe (Ratio a) where
  universe :: [Ratio a]
universe = [Ratio a]
forall a. RationalUniverse a => [Ratio a]
rationalUniverse

class RationalUniverse a where
  rationalUniverse :: [Ratio a]

instance RationalUniverse Integer where
    -- Why force the negations and reciprocals? This is more expensive if we
    -- ignore most of the result: it allocates four words (generally) for a
    -- negative element rather than two words for a thunk that will evaluate to
    -- one. But it's presumably more common to use the elements in a universe
    -- than to leap over them, so we optimize for the former case. We
    -- interleave manually to avoid allocating four intermediate lists.
    rationalUniverse :: [Ratio Integer]
rationalUniverse = Ratio Integer
0 Ratio Integer -> [Ratio Integer] -> [Ratio Integer]
forall a. a -> [a] -> [a]
: Ratio Integer
1 Ratio Integer -> [Ratio Integer] -> [Ratio Integer]
forall a. a -> [a] -> [a]
: (-Ratio Integer
1) Ratio Integer -> [Ratio Integer] -> [Ratio Integer]
forall a. a -> [a] -> [a]
: Stream (Ratio Integer) -> [Ratio Integer]
forall a. Integral a => Stream (Ratio a) -> [Ratio a]
go Stream (Ratio Integer)
forall a. Integral a => Stream (Ratio a)
leftSideStream
      where
        go :: Stream (Ratio a) -> [Ratio a]
go (x :: Ratio a
x@(a
xn :% a
xd) :< Stream (Ratio a)
xs) =
          let !nx :: Ratio a
nx = -Ratio a
x
              !rx :: Ratio a
rx = a
xd a -> a -> Ratio a
forall a. a -> a -> Ratio a
:% a
xn
              !nrx :: Ratio a
nrx = -Ratio a
rx
          in Ratio a
x Ratio a -> [Ratio a] -> [Ratio a]
forall a. a -> [a] -> [a]
: Ratio a
rx Ratio a -> [Ratio a] -> [Ratio a]
forall a. a -> [a] -> [a]
: Ratio a
nx Ratio a -> [Ratio a] -> [Ratio a]
forall a. a -> [a] -> [a]
: Ratio a
nrx Ratio a -> [Ratio a] -> [Ratio a]
forall a. a -> [a] -> [a]
: Stream (Ratio a) -> [Ratio a]
go Stream (Ratio a)
xs

instance RationalUniverse Natural where
    rationalUniverse :: [Ratio Natural]
rationalUniverse = Ratio Natural
0 Ratio Natural -> [Ratio Natural] -> [Ratio Natural]
forall a. a -> [a] -> [a]
: Ratio Natural
1 Ratio Natural -> [Ratio Natural] -> [Ratio Natural]
forall a. a -> [a] -> [a]
: Stream (Ratio Natural) -> [Ratio Natural]
forall a. Stream (Ratio a) -> [Ratio a]
go Stream (Ratio Natural)
forall a. Integral a => Stream (Ratio a)
leftSideStream
      where
        go :: Stream (Ratio a) -> [Ratio a]
go (x :: Ratio a
x@(a
xn :% a
xd) :< Stream (Ratio a)
xs) =
          let !rx :: Ratio a
rx = a
xd a -> a -> Ratio a
forall a. a -> a -> Ratio a
:% a
xn
          in Ratio a
x Ratio a -> [Ratio a] -> [Ratio a]
forall a. a -> [a] -> [a]
: Ratio a
rx Ratio a -> [Ratio a] -> [Ratio a]
forall a. a -> [a] -> [a]
: Stream (Ratio a) -> [Ratio a]
go Stream (Ratio a)
xs

-------------------------------------------------------------------------------
--
-------------------------------------------------------------------------------

-- |
-- >>> mapM_ print (universe :: [Bool -> Bool])
-- [(False,False),(True,False)]
-- [(False,False),(True,True)]
-- [(False,True),(True,False)]
-- [(False,True),(True,True)]
--
instance (Finite a, Ord a, Universe b) => Universe (a -> b) where
  -- could change the Ord constraint to an Eq one, but come on, how many finite
  -- types can't be ordered?
  universe :: [a -> b]
universe = ([b] -> a -> b) -> [[b]] -> [a -> b]
forall a b. (a -> b) -> [a] -> [b]
map [b] -> a -> b
tableToFunction [[b]]
tables where
    tables :: [[b]]
tables          = [[b]] -> [[b]]
forall a. [[a]] -> [[a]]
choices [[b]
forall a. Universe a => [a]
universe | a
_ <- [a]
monoUniverse]
    tableToFunction :: [b] -> a -> b
tableToFunction = (!) (Map a b -> a -> b) -> ([b] -> Map a b) -> [b] -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, b)] -> Map a b
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(a, b)] -> Map a b) -> ([b] -> [(a, b)]) -> [b] -> Map a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
monoUniverse
    monoUniverse :: [a]
monoUniverse    = [a]
forall a. Finite a => [a]
universeF

instance Finite ()       where cardinality :: Tagged () Natural
cardinality = Tagged () Natural
1
instance Finite Bool     where cardinality :: Tagged Bool Natural
cardinality = Tagged Bool Natural
2
instance Finite Char     where cardinality :: Tagged Char Natural
cardinality = Tagged Char Natural
1114112
instance Finite Ordering where cardinality :: Tagged Ordering Natural
cardinality = Tagged Ordering Natural
3
instance Finite Int      where cardinality :: Tagged Int Natural
cardinality = Int -> Tagged Int Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
maxBound :: Int) Tagged Int Natural -> Tagged Int Natural -> Tagged Int Natural
forall a. Num a => a -> a -> a
- Int -> Tagged Int Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
minBound :: Int) Tagged Int Natural -> Tagged Int Natural -> Tagged Int Natural
forall a. Num a => a -> a -> a
+ Tagged Int Natural
1
instance Finite Int8     where cardinality :: Tagged Int8 Natural
cardinality = Tagged Int8 Natural
2Tagged Int8 Natural -> Integer -> Tagged Int8 Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
8
instance Finite Int16    where cardinality :: Tagged Int16 Natural
cardinality = Tagged Int16 Natural
2Tagged Int16 Natural -> Integer -> Tagged Int16 Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
16
instance Finite Int32    where cardinality :: Tagged Int32 Natural
cardinality = Tagged Int32 Natural
2Tagged Int32 Natural -> Integer -> Tagged Int32 Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
32
instance Finite Int64    where cardinality :: Tagged Int64 Natural
cardinality = Tagged Int64 Natural
2Tagged Int64 Natural -> Integer -> Tagged Int64 Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
64
instance Finite Word     where cardinality :: Tagged Word Natural
cardinality = Word -> Tagged Word Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word
forall a. Bounded a => a
maxBound :: Word) Tagged Word Natural -> Tagged Word Natural -> Tagged Word Natural
forall a. Num a => a -> a -> a
- Word -> Tagged Word Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word
forall a. Bounded a => a
minBound :: Word) Tagged Word Natural -> Tagged Word Natural -> Tagged Word Natural
forall a. Num a => a -> a -> a
+ Tagged Word Natural
1
instance Finite Word8    where cardinality :: Tagged Word8 Natural
cardinality = Natural -> Tagged Word8 Natural
forall k (s :: k) b. b -> Tagged s b
Tagged (Natural -> Tagged Word8 Natural)
-> Natural -> Tagged Word8 Natural
forall a b. (a -> b) -> a -> b
$ Natural
2Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
8
instance Finite Word16   where cardinality :: Tagged Word16 Natural
cardinality = Natural -> Tagged Word16 Natural
forall k (s :: k) b. b -> Tagged s b
Tagged (Natural -> Tagged Word16 Natural)
-> Natural -> Tagged Word16 Natural
forall a b. (a -> b) -> a -> b
$ Natural
2Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
16
instance Finite Word32   where cardinality :: Tagged Word32 Natural
cardinality = Natural -> Tagged Word32 Natural
forall k (s :: k) b. b -> Tagged s b
Tagged (Natural -> Tagged Word32 Natural)
-> Natural -> Tagged Word32 Natural
forall a b. (a -> b) -> a -> b
$ Natural
2Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
32
instance Finite Word64   where cardinality :: Tagged Word64 Natural
cardinality = Natural -> Tagged Word64 Natural
forall k (s :: k) b. b -> Tagged s b
Tagged (Natural -> Tagged Word64 Natural)
-> Natural -> Tagged Word64 Natural
forall a b. (a -> b) -> a -> b
$ Natural
2Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
64

instance  Finite a            => Finite (Maybe  a  ) where
    cardinality :: Tagged (Maybe a) Natural
cardinality = (Natural -> Natural)
-> Tagged (Maybe a) Natural -> Tagged (Maybe a) Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Natural -> Natural
forall a. Enum a => a -> a
succ (Tagged a Natural -> Tagged (Maybe a) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural))
instance (Finite a, Finite b) => Finite (Either a b) where
  universeF :: [Either a b]
universeF = (a -> Either a b) -> [a] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Either a b
forall a b. a -> Either a b
Left [a]
forall a. Universe a => [a]
universe [Either a b] -> [Either a b] -> [Either a b]
forall a. [a] -> [a] -> [a]
++ (b -> Either a b) -> [b] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map b -> Either a b
forall a b. b -> Either a b
Right [b]
forall a. Universe a => [a]
universe
  cardinality :: Tagged (Either a b) Natural
cardinality = (Natural -> Natural -> Natural)
-> Tagged (Either a b) Natural
-> Tagged (Either a b) Natural
-> Tagged (Either a b) Natural
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Natural
a Natural
b -> Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
b)
    (Tagged a Natural -> Tagged (Either a b) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural))
    (Tagged b Natural -> Tagged (Either a b) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged b Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged b Natural))

instance (Finite a, Finite b) => Finite (a, b) where
  universeF :: [(a, b)]
universeF = (a -> b -> (a, b)) -> [a] -> [b] -> [(a, b)]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) [a]
forall a. Finite a => [a]
universeF [b]
forall a. Finite a => [a]
universeF
  cardinality :: Tagged (a, b) Natural
cardinality = (Natural -> Natural -> Natural)
-> Tagged (a, b) Natural
-> Tagged (a, b) Natural
-> Tagged (a, b) Natural
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Natural
a Natural
b -> Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
b)
    (Tagged a Natural -> Tagged (a, b) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural))
    (Tagged b Natural -> Tagged (a, b) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged b Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged b Natural))

instance (Finite a, Finite b, Finite c) => Finite (a, b, c) where
  universeF :: [(a, b, c)]
universeF = (a -> b -> c -> (a, b, c)) -> [a] -> [b] -> [c] -> [(a, b, c)]
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (,,) [a]
forall a. Finite a => [a]
universeF [b]
forall a. Finite a => [a]
universeF [c]
forall a. Finite a => [a]
universeF
  cardinality :: Tagged (a, b, c) Natural
cardinality = (Natural -> Natural -> Natural -> Natural)
-> Tagged (a, b, c) Natural
-> Tagged (a, b, c) Natural
-> Tagged (a, b, c) Natural
-> Tagged (a, b, c) Natural
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (\Natural
a Natural
b Natural
c -> Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
b Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
c)
    (Tagged a Natural -> Tagged (a, b, c) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural))
    (Tagged b Natural -> Tagged (a, b, c) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged b Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged b Natural))
    (Tagged c Natural -> Tagged (a, b, c) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged c Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged c Natural))

instance (Finite a, Finite b, Finite c, Finite d) => Finite (a, b, c, d) where
  universeF :: [(a, b, c, d)]
universeF = (a -> b -> c -> d -> (a, b, c, d))
-> [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
forall (m :: * -> *) a1 a2 a3 a4 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
liftM4 (,,,) [a]
forall a. Finite a => [a]
universeF [b]
forall a. Finite a => [a]
universeF [c]
forall a. Finite a => [a]
universeF [d]
forall a. Finite a => [a]
universeF
  cardinality :: Tagged (a, b, c, d) Natural
cardinality = (Natural -> Natural -> Natural -> Natural -> Natural)
-> Tagged (a, b, c, d) Natural
-> Tagged (a, b, c, d) Natural
-> Tagged (a, b, c, d) Natural
-> Tagged (a, b, c, d) Natural
-> Tagged (a, b, c, d) Natural
forall (m :: * -> *) a1 a2 a3 a4 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
liftM4 (\Natural
a Natural
b Natural
c Natural
d -> Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
b Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
c Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
d)
    (Tagged a Natural -> Tagged (a, b, c, d) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural))
    (Tagged b Natural -> Tagged (a, b, c, d) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged b Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged b Natural))
    (Tagged c Natural -> Tagged (a, b, c, d) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged c Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged c Natural))
    (Tagged d Natural -> Tagged (a, b, c, d) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged d Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged d Natural))

instance (Finite a, Finite b, Finite c, Finite d, Finite e) => Finite (a, b, c, d, e) where
  universeF :: [(a, b, c, d, e)]
universeF = (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]
forall (m :: * -> *) a1 a2 a3 a4 a5 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> a5 -> r)
-> m a1 -> m a2 -> m a3 -> m a4 -> m a5 -> m r
liftM5 (,,,,) [a]
forall a. Finite a => [a]
universeF [b]
forall a. Finite a => [a]
universeF [c]
forall a. Finite a => [a]
universeF [d]
forall a. Finite a => [a]
universeF [e]
forall a. Finite a => [a]
universeF
  cardinality :: Tagged (a, b, c, d, e) Natural
cardinality = (Natural -> Natural -> Natural -> Natural -> Natural -> Natural)
-> Tagged (a, b, c, d, e) Natural
-> Tagged (a, b, c, d, e) Natural
-> Tagged (a, b, c, d, e) Natural
-> Tagged (a, b, c, d, e) Natural
-> Tagged (a, b, c, d, e) Natural
-> Tagged (a, b, c, d, e) Natural
forall (m :: * -> *) a1 a2 a3 a4 a5 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> a5 -> r)
-> m a1 -> m a2 -> m a3 -> m a4 -> m a5 -> m r
liftM5 (\Natural
a Natural
b Natural
c Natural
d Natural
e -> Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
b Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
c Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
d Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
e)
    (Tagged a Natural -> Tagged (a, b, c, d, e) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural))
    (Tagged b Natural -> Tagged (a, b, c, d, e) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged b Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged b Natural))
    (Tagged c Natural -> Tagged (a, b, c, d, e) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged c Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged c Natural))
    (Tagged d Natural -> Tagged (a, b, c, d, e) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged d Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged d Natural))
    (Tagged e Natural -> Tagged (a, b, c, d, e) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged e Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged e Natural))

instance Finite Mon.All where universeF :: [All]
universeF = (Bool -> All) -> [Bool] -> [All]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> All
Mon.All [Bool]
forall a. Finite a => [a]
universeF; cardinality :: Tagged All Natural
cardinality = Tagged All Natural
2
instance Finite Mon.Any where universeF :: [Any]
universeF = (Bool -> Any) -> [Bool] -> [Any]
forall a b. (a -> b) -> [a] -> [b]
map Bool -> Any
Mon.Any [Bool]
forall a. Finite a => [a]
universeF; cardinality :: Tagged Any Natural
cardinality = Tagged Any Natural
2
instance Finite a => Finite (Mon.Sum     a) where universeF :: [Sum a]
universeF = (a -> Sum a) -> [a] -> [Sum a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Sum a
forall a. a -> Sum a
Mon.Sum     [a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Sum a) Natural
cardinality = (a -> Sum a) -> Tagged a Natural -> Tagged (Sum a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> Sum a
forall a. a -> Sum a
Mon.Sum     Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality
instance Finite a => Finite (Mon.Product a) where universeF :: [Product a]
universeF = (a -> Product a) -> [a] -> [Product a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Product a
forall a. a -> Product a
Mon.Product [a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Product a) Natural
cardinality = (a -> Product a) -> Tagged a Natural -> Tagged (Product a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> Product a
forall a. a -> Product a
Mon.Product Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality
instance Finite a => Finite (Mon.Dual    a) where universeF :: [Dual a]
universeF = (a -> Dual a) -> [a] -> [Dual a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Dual a
forall a. a -> Dual a
Mon.Dual    [a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Dual a) Natural
cardinality = (a -> Dual a) -> Tagged a Natural -> Tagged (Dual a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> Dual a
forall a. a -> Dual a
Mon.Dual    Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality
instance Finite a => Finite (Mon.First   a) where universeF :: [First a]
universeF = (Maybe a -> First a) -> [Maybe a] -> [First a]
forall a b. (a -> b) -> [a] -> [b]
map Maybe a -> First a
forall a. Maybe a -> First a
Mon.First   [Maybe a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (First a) Natural
cardinality = (Maybe a -> First a)
-> Tagged (Maybe a) Natural -> Tagged (First a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith Maybe a -> First a
forall a. Maybe a -> First a
Mon.First   Tagged (Maybe a) Natural
forall a. Finite a => Tagged a Natural
cardinality
instance Finite a => Finite (Mon.Last    a) where universeF :: [Last a]
universeF = (Maybe a -> Last a) -> [Maybe a] -> [Last a]
forall a b. (a -> b) -> [a] -> [b]
map Maybe a -> Last a
forall a. Maybe a -> Last a
Mon.Last    [Maybe a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Last a) Natural
cardinality = (Maybe a -> Last a)
-> Tagged (Maybe a) Natural -> Tagged (Last a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith Maybe a -> Last a
forall a. Maybe a -> Last a
Mon.Last    Tagged (Maybe a) Natural
forall a. Finite a => Tagged a Natural
cardinality

instance Finite a => Finite (Semi.Max   a) where universeF :: [Max a]
universeF = (a -> Max a) -> [a] -> [Max a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Max a
forall a. a -> Max a
Semi.Max   [a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Max a) Natural
cardinality = (a -> Max a) -> Tagged a Natural -> Tagged (Max a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> Max a
forall a. a -> Max a
Semi.Max   Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality
instance Finite a => Finite (Semi.Min   a) where universeF :: [Min a]
universeF = (a -> Min a) -> [a] -> [Min a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Min a
forall a. a -> Min a
Semi.Min   [a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Min a) Natural
cardinality = (a -> Min a) -> Tagged a Natural -> Tagged (Min a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> Min a
forall a. a -> Min a
Semi.Min   Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality
instance Finite a => Finite (Semi.First a) where universeF :: [First a]
universeF = (a -> First a) -> [a] -> [First a]
forall a b. (a -> b) -> [a] -> [b]
map a -> First a
forall a. a -> First a
Semi.First [a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (First a) Natural
cardinality = (a -> First a) -> Tagged a Natural -> Tagged (First a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> First a
forall a. a -> First a
Semi.First Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality
instance Finite a => Finite (Semi.Last  a) where universeF :: [Last a]
universeF = (a -> Last a) -> [a] -> [Last a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Last a
forall a. a -> Last a
Semi.Last  [a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Last a) Natural
cardinality = (a -> Last a) -> Tagged a Natural -> Tagged (Last a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> Last a
forall a. a -> Last a
Semi.Last  Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality

-- |
-- >>> mapM_ print (universeF :: [Bool -> Bool])
-- [(False,False),(True,False)]
-- [(False,False),(True,True)]
-- [(False,True),(True,False)]
-- [(False,True),(True,True)]
--
-- >>> cardinality :: Tagged (Bool -> Ordering) Natural
-- Tagged 9
--
-- >>> cardinality :: Tagged (Ordering -> Bool) Natural
-- Tagged 8
--
instance (Ord a, Finite a, Finite b) => Finite (a -> b) where
  universeF :: [a -> b]
universeF = ([b] -> a -> b) -> [[b]] -> [a -> b]
forall a b. (a -> b) -> [a] -> [b]
map [b] -> a -> b
tableToFunction [[b]]
tables where
    tables :: [[b]]
tables          = [[b]] -> [[b]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[b]
forall a. Finite a => [a]
universeF | a
_ <- [a]
monoUniverse]
    tableToFunction :: [b] -> a -> b
tableToFunction = (!) (Map a b -> a -> b) -> ([b] -> Map a b) -> [b] -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, b)] -> Map a b
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(a, b)] -> Map a b) -> ([b] -> [(a, b)]) -> [b] -> Map a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
monoUniverse
    monoUniverse :: [a]
monoUniverse    = [a]
forall a. Finite a => [a]
universeF
  cardinality :: Tagged (a -> b) Natural
cardinality = (Natural -> Natural -> Natural)
-> Tagged (a -> b) Natural
-> Tagged (a -> b) Natural
-> Tagged (a -> b) Natural
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
(^)
    (Tagged b Natural -> Tagged (a -> b) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged b Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged b Natural))
    (Tagged a Natural -> Tagged (a -> b) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural))

-- to add when somebody asks for it: instance (Eq a, Finite a) => Finite (Endo a) (+Universe)

-------------------------------------------------------------------------------
-- void
-------------------------------------------------------------------------------

instance Universe Void where universe :: [Void]
universe = []
instance Finite Void where cardinality :: Tagged Void Natural
cardinality = Tagged Void Natural
0

-------------------------------------------------------------------------------
-- tagged
-------------------------------------------------------------------------------

instance Universe (Proxy a) where universe :: [Proxy a]
universe = [Proxy a
forall k (t :: k). Proxy t
Proxy]
instance Finite (Proxy a) where cardinality :: Tagged (Proxy a) Natural
cardinality = Tagged (Proxy a) Natural
1

instance Universe a => Universe (Tagged b a) where universe :: [Tagged b a]
universe = (a -> Tagged b a) -> [a] -> [Tagged b a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Tagged b a
forall k (s :: k) b. b -> Tagged s b
Tagged [a]
forall a. Universe a => [a]
universe
instance Finite a => Finite (Tagged b a) where cardinality :: Tagged (Tagged b a) Natural
cardinality = (a -> Tagged b a)
-> Tagged a Natural -> Tagged (Tagged b a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> Tagged b a
forall k (s :: k) b. b -> Tagged s b
Tagged Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality

-------------------------------------------------------------------------------
-- containers
-------------------------------------------------------------------------------

-- |
-- >>> import qualified Data.Set as Set
-- >>> mapM_ print (universe :: [Set.Set Bool])
-- fromList []
-- fromList [False]
-- fromList [True]
-- fromList [False,True]
--
instance (Ord a, Universe a) => Universe (Set.Set a) where
    universe :: [Set a]
universe = Set a
forall a. Set a
Set.empty Set a -> [Set a] -> [Set a]
forall a. a -> [a] -> [a]
: [a] -> [Set a]
forall a. Ord a => [a] -> [Set a]
go [a]
forall a. Universe a => [a]
universe
      where
        go :: [a] -> [Set a]
go []     = []
        go (a
x:[a]
xs) = a -> Set a
forall a. a -> Set a
Set.singleton a
x Set a -> [Set a] -> [Set a]
forall a. a -> [a] -> [a]
: [Set a] -> [Set a]
inter ([a] -> [Set a]
go [a]
xs)
          where
            -- Probably more efficient than using (+++)
            inter :: [Set a] -> [Set a]
inter []     = []
            inter (Set a
y:[Set a]
ys) = Set a
y Set a -> [Set a] -> [Set a]
forall a. a -> [a] -> [a]
: a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
x Set a
y Set a -> [Set a] -> [Set a]
forall a. a -> [a] -> [a]
: [Set a] -> [Set a]
inter [Set a]
ys

instance (Ord a, Finite a) => Finite (Set.Set a) where
    cardinality :: Tagged (Set a) Natural
cardinality = Tagged a Natural -> Tagged (Set a) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag ((Natural -> Natural) -> Tagged a Natural -> Tagged a Natural
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Natural
2 Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^) (Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural))

-- |
-- >>> import qualified Data.Map as Map
-- >>> mapM_ print (universe :: [Map.Map Bool Bool])
-- fromList []
-- fromList [(True,False)]
-- fromList [(False,False)]
-- fromList [(True,True)]
-- fromList [(False,False),(True,False)]
-- fromList [(False,True)]
-- fromList [(False,False),(True,True)]
-- fromList [(False,True),(True,False)]
-- fromList [(False,True),(True,True)]
--
--
instance (Ord k, Finite k, Universe v) => Universe (Map.Map k v) where
  universe :: [Map k v]
universe = ([Maybe v] -> Map k v) -> [[Maybe v]] -> [Map k v]
forall a b. (a -> b) -> [a] -> [b]
map [Maybe v] -> Map k v
tableToFunction [[Maybe v]]
tables where
    tables :: [[Maybe v]]
tables          = [[Maybe v]] -> [[Maybe v]]
forall a. [[a]] -> [[a]]
choices [[Maybe v]
forall a. Universe a => [a]
universe | k
_ <- [k]
monoUniverse]
    tableToFunction :: [Maybe v] -> Map k v
tableToFunction = [(k, Maybe v)] -> Map k v
forall k a. Ord k => [(k, Maybe a)] -> Map k a
fromList' ([(k, Maybe v)] -> Map k v)
-> ([Maybe v] -> [(k, Maybe v)]) -> [Maybe v] -> Map k v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [k] -> [Maybe v] -> [(k, Maybe v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [k]
monoUniverse
    monoUniverse :: [k]
monoUniverse    = [k]
forall a. Finite a => [a]
universeF
    fromList' :: [(k, Maybe a)] -> Map k a
fromList' [(k, Maybe a)]
xs = [(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (k
k,a
v) | (k
k, Just a
v) <- [(k, Maybe a)]
xs ]

instance (Ord k, Finite k, Finite v) => Finite (Map.Map k v) where
  universeF :: [Map k v]
universeF = ([Maybe v] -> Map k v) -> [[Maybe v]] -> [Map k v]
forall a b. (a -> b) -> [a] -> [b]
map [Maybe v] -> Map k v
tableToFunction [[Maybe v]]
tables where
    tables :: [[Maybe v]]
tables          = [[Maybe v]] -> [[Maybe v]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[Maybe v]
forall a. Finite a => [a]
universeF | k
_ <- [k]
monoUniverse]
    tableToFunction :: [Maybe v] -> Map k v
tableToFunction = [(k, Maybe v)] -> Map k v
forall k a. Ord k => [(k, Maybe a)] -> Map k a
fromList' ([(k, Maybe v)] -> Map k v)
-> ([Maybe v] -> [(k, Maybe v)]) -> [Maybe v] -> Map k v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [k] -> [Maybe v] -> [(k, Maybe v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [k]
monoUniverse
    monoUniverse :: [k]
monoUniverse    = [k]
forall a. Finite a => [a]
universeF
    fromList' :: [(k, Maybe a)] -> Map k a
fromList' [(k, Maybe a)]
xs = [(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (k
k,a
v) | (k
k, Just a
v) <- [(k, Maybe a)]
xs ]

  cardinality :: Tagged (Map k v) Natural
cardinality = (Natural -> Natural -> Natural)
-> Tagged (Map k v) Natural
-> Tagged (Map k v) Natural
-> Tagged (Map k v) Natural
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Natural
b Natural
a -> (Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
b) Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Natural
a)
    (Tagged v Natural -> Tagged (Map k v) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged v Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged v Natural))
    (Tagged k Natural -> Tagged (Map k v) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged k Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged k Natural))

-------------------------------------------------------------------------------
-- transformers
-------------------------------------------------------------------------------

instance  Universe  a => Universe (Const a b) where universe :: [Const a b]
universe  = (a -> Const a b) -> [a] -> [Const a b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Const a b
forall k a (b :: k). a -> Const a b
Const [a]
forall a. Universe a => [a]
universe
instance  Finite    a => Finite   (Const a b) where universeF :: [Const a b]
universeF = (a -> Const a b) -> [a] -> [Const a b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Const a b
forall k a (b :: k). a -> Const a b
Const [a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Const a b) Natural
cardinality = (a -> Const a b) -> Tagged a Natural -> Tagged (Const a b) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> Const a b
forall k a (b :: k). a -> Const a b
Const Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality

instance  Universe    a                    => Universe (Identity    a) where universe :: [Identity a]
universe  = (a -> Identity a) -> [a] -> [Identity a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Identity a
forall a. a -> Identity a
Identity  [a]
forall a. Universe a => [a]
universe
instance  Universe (f a)                   => Universe (IdentityT f a) where universe :: [IdentityT f a]
universe  = (f a -> IdentityT f a) -> [f a] -> [IdentityT f a]
forall a b. (a -> b) -> [a] -> [b]
map f a -> IdentityT f a
forall k (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT [f a]
forall a. Universe a => [a]
universe
instance (Finite e, Ord e, Universe (m a)) => Universe (ReaderT e m a) where universe :: [ReaderT e m a]
universe  = ((e -> m a) -> ReaderT e m a) -> [e -> m a] -> [ReaderT e m a]
forall a b. (a -> b) -> [a] -> [b]
map (e -> m a) -> ReaderT e m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT   [e -> m a]
forall a. Universe a => [a]
universe
instance  Universe (f (g a))               => Universe (Compose f g a) where universe :: [Compose f g a]
universe  = (f (g a) -> Compose f g a) -> [f (g a)] -> [Compose f g a]
forall a b. (a -> b) -> [a] -> [b]
map f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose   [f (g a)]
forall a. Universe a => [a]
universe
instance (Universe (f a), Universe (g a))  => Universe (Product f g a) where universe :: [Product f g a]
universe  = [f a -> g a -> Product f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair f a
f g a
g | (f a
f, g a
g) <- [f a]
forall a. Universe a => [a]
universe [f a] -> [g a] -> [(f a, g a)]
forall a b. [a] -> [b] -> [(a, b)]
+*+ [g a]
forall a. Universe a => [a]
universe]
instance (Universe (f a), Universe (g a))  => Universe (Sum     f g a) where universe :: [Sum f g a]
universe  = (f a -> Sum f g a) -> [f a] -> [Sum f g a]
forall a b. (a -> b) -> [a] -> [b]
map f a -> Sum f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL [f a]
forall a. Universe a => [a]
universe [Sum f g a] -> [Sum f g a] -> [Sum f g a]
forall a. [a] -> [a] -> [a]
+++ (g a -> Sum f g a) -> [g a] -> [Sum f g a]
forall a b. (a -> b) -> [a] -> [b]
map g a -> Sum f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR [g a]
forall a. Universe a => [a]
universe

instance  Finite       a                   => Finite   (Identity    a) where universeF :: [Identity a]
universeF = (a -> Identity a) -> [a] -> [Identity a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Identity a
forall a. a -> Identity a
Identity  [a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Identity a) Natural
cardinality = (a -> Identity a)
-> Tagged a Natural -> Tagged (Identity a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith a -> Identity a
forall a. a -> Identity a
Identity  Tagged a Natural
forall a. Finite a => Tagged a Natural
cardinality
instance  Finite    (f a)                  => Finite   (IdentityT f a) where universeF :: [IdentityT f a]
universeF = (f a -> IdentityT f a) -> [f a] -> [IdentityT f a]
forall a b. (a -> b) -> [a] -> [b]
map f a -> IdentityT f a
forall k (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT [f a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (IdentityT f a) Natural
cardinality = (f a -> IdentityT f a)
-> Tagged (f a) Natural -> Tagged (IdentityT f a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith f a -> IdentityT f a
forall k (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT Tagged (f a) Natural
forall a. Finite a => Tagged a Natural
cardinality
instance (Finite e, Ord e, Finite   (m a)) => Finite   (ReaderT e m a) where universeF :: [ReaderT e m a]
universeF = ((e -> m a) -> ReaderT e m a) -> [e -> m a] -> [ReaderT e m a]
forall a b. (a -> b) -> [a] -> [b]
map (e -> m a) -> ReaderT e m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT   [e -> m a]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (ReaderT e m a) Natural
cardinality = ((e -> m a) -> ReaderT e m a)
-> Tagged (e -> m a) Natural -> Tagged (ReaderT e m a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith (e -> m a) -> ReaderT e m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT   Tagged (e -> m a) Natural
forall a. Finite a => Tagged a Natural
cardinality
instance  Finite (f (g a))                 => Finite   (Compose f g a) where universeF :: [Compose f g a]
universeF = (f (g a) -> Compose f g a) -> [f (g a)] -> [Compose f g a]
forall a b. (a -> b) -> [a] -> [b]
map f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose   [f (g a)]
forall a. Finite a => [a]
universeF; cardinality :: Tagged (Compose f g a) Natural
cardinality = (f (g a) -> Compose f g a)
-> Tagged (f (g a)) Natural -> Tagged (Compose f g a) Natural
forall a b x. (a -> b) -> Tagged a x -> Tagged b x
retagWith f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose   Tagged (f (g a)) Natural
forall a. Finite a => Tagged a Natural
cardinality
instance (Finite (f a), Finite (g a))      => Finite   (Product f g a) where
  universeF :: [Product f g a]
universeF = (f a -> g a -> Product f g a) -> [f a] -> [g a] -> [Product f g a]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 f a -> g a -> Product f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair [f a]
forall a. Finite a => [a]
universeF [g a]
forall a. Finite a => [a]
universeF
  cardinality :: Tagged (Product f g a) Natural
cardinality = (Natural -> Natural -> Natural)
-> Tagged (Product f g a) Natural
-> Tagged (Product f g a) Natural
-> Tagged (Product f g a) Natural
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(*)
    (Tagged (f a) Natural -> Tagged (Product f g a) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (f a) Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged (f a) Natural))
    (Tagged (g a) Natural -> Tagged (Product f g a) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (g a) Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged (g a) Natural))
instance (Finite (f a), Finite (g a))      => Finite   (Sum f g a) where
  universeF :: [Sum f g a]
universeF =  (f a -> Sum f g a) -> [f a] -> [Sum f g a]
forall a b. (a -> b) -> [a] -> [b]
map f a -> Sum f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL [f a]
forall a. Universe a => [a]
universe [Sum f g a] -> [Sum f g a] -> [Sum f g a]
forall a. [a] -> [a] -> [a]
++ (g a -> Sum f g a) -> [g a] -> [Sum f g a]
forall a b. (a -> b) -> [a] -> [b]
map g a -> Sum f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR [g a]
forall a. Universe a => [a]
universe
  cardinality :: Tagged (Sum f g a) Natural
cardinality = (Natural -> Natural -> Natural)
-> Tagged (Sum f g a) Natural
-> Tagged (Sum f g a) Natural
-> Tagged (Sum f g a) Natural
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(+)
    (Tagged (f a) Natural -> Tagged (Sum f g a) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (f a) Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged (f a) Natural))
    (Tagged (g a) Natural -> Tagged (Sum f g a) Natural
forall k1 k2 (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (Tagged (g a) Natural
forall a. Finite a => Tagged a Natural
cardinality :: Tagged (g a) Natural))