-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Nat and Fin: peano naturals and finite numbers -- -- This package provides two simple types, and some tools to work with -- them. Also on type level as DataKinds. -- -- 
--   -- Peano naturals
--   data Nat = Z | S Nat
--   
--   -- Finite naturals
--   data Fin (n :: Nat) where
--       Z :: Fin ('S n)
--       S :: Fin n -> Fin ('Nat.S n)
--
-- -- vec implements length-indexed (sized) lists using this package -- for indexes. -- -- The Data.Fin.Enum module let's work generically with -- enumerations. -- -- See Hasochism: the pleasure and pain of dependently typed haskell -- programming by Sam Lindley and Conor McBride for answers to -- how and why. Read APLicative Programming with -- Naperian Functors by Jeremy Gibbons for (not so) different ones. -- --

Similar packages

-- -- @package fin @version 0.2 -- | Nat numbers. -- -- This module is designed to be imported qualified. module Data.Nat -- | Nat natural numbers. -- -- Better than GHC's built-in Nat for some use cases. data Nat Z :: Nat S :: Nat -> Nat -- | Convert Nat to Natural -- -- 
--   >>> toNatural 0
--   0
--
-- -- 
--   >>> toNatural 2
--   2
--
-- -- 
--   >>> toNatural $ S $ S $ Z
--   2
--
toNatural :: Nat -> Natural -- | Convert Natural to Nat -- -- 
--   >>> fromNatural 4
--   4
--
-- -- 
--   >>> explicitShow (fromNatural 4)
--   "S (S (S (S Z)))"
--
fromNatural :: Natural -> Nat -- | Fold Nat. -- -- 
--   >>> cata [] ('x' :) 2
--   "xx"
--
cata :: a -> (a -> a) -> Nat -> a -- | show displaying a structure of Nat. -- -- 
--   >>> explicitShow 0
--   "Z"
--
-- -- 
--   >>> explicitShow 2
--   "S (S Z)"
--
explicitShow :: Nat -> String -- | showsPrec displaying a structure of Nat. explicitShowsPrec :: Int -> Nat -> ShowS nat0 :: Nat nat1 :: Nat nat2 :: Nat nat3 :: Nat nat4 :: Nat nat5 :: Nat nat6 :: Nat nat7 :: Nat nat8 :: Nat nat9 :: Nat instance Data.Data.Data Data.Nat.Nat instance GHC.Classes.Eq Data.Nat.Nat instance GHC.Show.Show Data.Nat.Nat instance GHC.Classes.Ord Data.Nat.Nat instance GHC.Num.Num Data.Nat.Nat instance GHC.Real.Real Data.Nat.Nat instance GHC.Real.Integral Data.Nat.Nat instance GHC.Enum.Enum Data.Nat.Nat instance Control.DeepSeq.NFData Data.Nat.Nat instance Data.Hashable.Class.Hashable Data.Nat.Nat instance Test.QuickCheck.Arbitrary.Arbitrary Data.Nat.Nat instance Test.QuickCheck.Arbitrary.CoArbitrary Data.Nat.Nat instance Test.QuickCheck.Function.Function Data.Nat.Nat instance Data.Universe.Class.Universe Data.Nat.Nat -- | Nat numbers. DataKinds stuff. -- -- This module re-exports Data.Nat, and adds type-level things. module Data.Type.Nat -- | Nat natural numbers. -- -- Better than GHC's built-in Nat for some use cases. data Nat Z :: Nat S :: Nat -> Nat -- | Convert Nat to Natural -- -- 
--   >>> toNatural 0
--   0
--
-- -- 
--   >>> toNatural 2
--   2
--
-- -- 
--   >>> toNatural $ S $ S $ Z
--   2
--
toNatural :: Nat -> Natural -- | Convert Natural to Nat -- -- 
--   >>> fromNatural 4
--   4
--
-- -- 
--   >>> explicitShow (fromNatural 4)
--   "S (S (S (S Z)))"
--
fromNatural :: Natural -> Nat -- | Fold Nat. -- -- 
--   >>> cata [] ('x' :) 2
--   "xx"
--
cata :: a -> (a -> a) -> Nat -> a -- | show displaying a structure of Nat. -- -- 
--   >>> explicitShow 0
--   "Z"
--
-- -- 
--   >>> explicitShow 2
--   "S (S Z)"
--
explicitShow :: Nat -> String -- | showsPrec displaying a structure of Nat. explicitShowsPrec :: Int -> Nat -> ShowS -- | Singleton of Nat. data SNat (n :: Nat) [SZ] :: SNat 'Z [SS] :: SNatI n => SNat ('S n) -- | Convert SNat to Nat. -- -- 
--   >>> snatToNat (snat :: SNat Nat1)
--   1
--
snatToNat :: forall n. SNat n -> Nat -- | Convert SNat to Natural -- -- 
--   >>> snatToNatural (snat :: SNat Nat0)
--   0
--
-- -- 
--   >>> snatToNatural (snat :: SNat Nat2)
--   2
--
snatToNatural :: forall n. SNat n -> Natural -- | Implicit SNat. -- -- In an unorthodox singleton way, it actually provides an induction -- function. -- -- The induction should often be fully inlined. See -- test/Inspection.hs. -- -- 
--   >>> :set -XPolyKinds
--   
--   >>> newtype Const a b = Const a deriving (Show)
--   
--   >>> induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3
--   Const 6
--
class SNatI (n :: Nat) induction :: SNatI n => f 'Z -> (forall m. SNatI m => f m -> f ('S m)) -> f n -- | Construct explicit SNat value. snat :: SNatI n => SNat n -- | Constructor SNatI dictionary from SNat. withSNat :: SNat n -> (SNatI n => r) -> r -- | Reify Nat. -- -- 
--   >>> reify nat3 reflect
--   3
--
reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r -- | Reflect type-level Nat to the term level. reflect :: forall n proxy. SNatI n => proxy n -> Nat -- | As reflect but with any Num. reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m -- | Decide equality of type-level numbers. -- -- 
--   >>> eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)
--   Just Refl
--
-- -- 
--   >>> eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)
--   Nothing
--
eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m) -- | Type family used to implement == from Data.Type.Equality -- module. type family EqNat (n :: Nat) (m :: Nat) -- | Decide equality of type-level numbers. -- -- 
--   >>> decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2))
--   "Yes Refl"
--
discreteNat :: forall n m. (SNatI n, SNatI m) => Dec (n :~: m) -- | Induction on Nat, functor form. Useful for computation. induction1 :: forall n f a. SNatI n => f 'Z a -> (forall m. SNatI m => f m a -> f ('S m) a) -> f n a -- | Unfold n steps of a general recursion. -- -- Note: Always benchmark. This function may give you both -- bad properties: a lot of code (increased binary size), and -- worse performance. -- -- For known n unfoldedFix will unfold recursion, for -- example -- -- 
--   unfoldedFix (Proxy :: Proxy Nat3) f = f (f (f (fix f)))
--
unfoldedFix :: forall n a proxy. SNatI n => proxy n -> (a -> a) -> a -- | Addition. -- -- 
--   >>> reflect (snat :: SNat (Plus Nat1 Nat2))
--   3
--
type family Plus (n :: Nat) (m :: Nat) :: Nat -- | Multiplication. -- -- 
--   >>> reflect (snat :: SNat (Mult Nat2 Nat3))
--   6
--
type family Mult (n :: Nat) (m :: Nat) :: Nat -- | Multiplication by two. Doubling. -- -- 
--   >>> reflect (snat :: SNat (Mult2 Nat4))
--   8
--
type family Mult2 (n :: Nat) :: Nat -- | Division by two. False is 0 and True is 1 as a -- remainder. -- -- 
--   >>> :kind! DivMod2 Nat7
--   DivMod2 Nat7 :: (Nat, Bool)
--   = '( 'S ('S ('S 'Z)), 'True)
--
-- -- 
--   >>> :kind! DivMod2 Nat4
--   DivMod2 Nat4 :: (Nat, Bool)
--   = '( 'S ('S 'Z), 'False)
--
type family DivMod2 (n :: Nat) :: (Nat, Bool) -- | Convert to GHC Nat. -- -- 
--   >>> :kind! ToGHC Nat5
--   ToGHC Nat5 :: GHC.Nat
--   = 5
--
type family ToGHC (n :: Nat) :: Nat -- | Convert from GHC Nat. -- -- 
--   >>> :kind! FromGHC 7
--   FromGHC 7 :: Nat
--   = 'S ('S ('S ('S ('S ('S ('S 'Z))))))
--
type family FromGHC (n :: Nat) :: Nat nat0 :: Nat nat1 :: Nat nat2 :: Nat nat3 :: Nat nat4 :: Nat nat5 :: Nat nat6 :: Nat nat7 :: Nat nat8 :: Nat nat9 :: Nat type Nat0 = 'Z type Nat1 = 'S Nat0 type Nat2 = 'S Nat1 type Nat3 = 'S Nat2 type Nat4 = 'S Nat3 type Nat5 = 'S Nat4 type Nat6 = 'S Nat5 type Nat7 = 'S Nat6 type Nat8 = 'S Nat7 type Nat9 = 'S Nat8 -- | 
--   0 + n = n
--
proofPlusZeroN :: Plus Nat0 n :~: n -- | 
--   n + 0 = n
--
proofPlusNZero :: SNatI n => Plus n Nat0 :~: n -- | 
--   0 * n = 0
--
proofMultZeroN :: Mult Nat0 n :~: Nat0 -- | 
--   n * 0 = 0
--
proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0 -- | 
--   1 * n = n
--
proofMultOneN :: SNatI n => Mult Nat1 n :~: n -- | 
--   n * 1 = n
--
proofMultNOne :: SNatI n => Mult n Nat1 :~: n instance GHC.Show.Show (Data.Type.Nat.SNat p) instance Data.Type.Equality.TestEquality @{Data.Nat.Nat} Data.Type.Nat.SNat instance Data.Type.Nat.SNatI 'Data.Nat.Z instance Data.Type.Nat.SNatI n => Data.Type.Nat.SNatI ('Data.Nat.S n) -- | Less-than-or-equal relation for (unary) natural numbers Nat. -- -- There are at least three ways to encode this relation. -- -- -- -- Depending on a situation, usage ergonomics are different. module Data.Type.Nat.LE -- | Total order of Nat, less-than-or-Equal-to, <math>. class LE n m leProof :: LE n m => LEProof n m -- | An evidence of <math>. zero+succ definition. data LEProof n m [LEZero] :: LEProof 'Z m [LESucc] :: LEProof n m -> LEProof ('S n) ('S m) -- | Constructor LE dictionary from LEProof. withLEProof :: LEProof n m -> (LE n m => r) -> r -- | Find the LEProof n m, i.e. compare numbers. decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m) -- | <math> leZero :: LEProof 'Z n -- | <math> leSucc :: LEProof n m -> LEProof ('S n) ('S m) -- | <math> leRefl :: forall n. SNatI n => LEProof n n -- | <math> leStep :: LEProof n m -> LEProof n ('S m) -- | <math> leAsym :: LEProof n m -> LEProof m n -> n :~: m -- | <math> leTrans :: LEProof n m -> LEProof m p -> LEProof n p -- | <math> leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n -- | <math> -- -- 
--   >>> leProof :: LEProof Nat2 Nat3
--   LESucc (LESucc LEZero)
--
-- -- 
--   >>> leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))
--   LESucc (LESucc (LESucc LEZero))
--
-- -- 
--   >>> lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))
--   LESucc (LESucc LEZero)
--
leSwap' :: LEProof n m -> LEProof ('S m) n -> void -- | <math> leStepL :: LEProof ('S n) m -> LEProof n m -- | <math> lePred :: LEProof ('S n) ('S m) -> LEProof n m -- | <math> proofZeroLEZero :: LEProof n 'Z -> n :~: 'Z instance GHC.Show.Show (Data.Type.Nat.LE.LEProof n m) instance Data.Type.Nat.LE.LE 'Data.Nat.Z m instance ((m :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.S m' :: Data.Nat.Nat), Data.Type.Nat.LE.LE n m') => Data.Type.Nat.LE.LE ('Data.Nat.S n) m instance GHC.Classes.Eq (Data.Type.Nat.LE.LEProof n m) instance GHC.Classes.Ord (Data.Type.Nat.LE.LEProof n m) instance (Data.Type.Nat.SNatI n, Data.Type.Nat.SNatI m) => Data.Type.Dec.Decidable (Data.Type.Nat.LE.LEProof n m) module Data.Type.Nat.LT -- | Less-Than-or. <math>. Well-founded relation on Nat. -- -- GHC can solve this for us! -- -- 
--   >>> ltProof :: LTProof Nat0 Nat4
--   LESucc LEZero
--
-- -- 
--   >>> ltProof :: LTProof Nat2 Nat4
--   LESucc (LESucc (LESucc LEZero))
--
-- -- 
--   >>> ltProof :: LTProof Nat3 Nat3
--   ...
--   ...error...
--   ...
--
class LT (n :: Nat) (m :: Nat) ltProof :: LT n m => LTProof n m -- | An evidence <math> which is the same as (1 + n le m). type LTProof n m = LEProof ('S n) m withLTProof :: LTProof n m -> (LT n m => r) -> r -- | <math> ltReflAbsurd :: LTProof n n -> a -- | <math> ltSymAbsurd :: LTProof n m -> LTProof m n -> a -- | <math> ltTrans :: LTProof n m -> LTProof m p -> LTProof n p instance Data.Type.Nat.LE.LE ('Data.Nat.S n) m => Data.Type.Nat.LT.LT n m module Data.Type.Nat.LE.ReflStep -- | An evidence of <math>. refl+step definition. data LEProof n m [LERefl] :: LEProof n n [LEStep] :: LEProof n m -> LEProof n ('S m) -- | Convert from zero+succ to refl+step definition. -- -- Inverse of toZeroSucc. fromZeroSucc :: forall n m. SNatI m => LEProof n m -> LEProof n m -- | Convert refl+step to zero+succ definition. -- -- Inverse of fromZeroSucc. toZeroSucc :: SNatI n => LEProof n m -> LEProof n m -- | Find the LEProof n m, i.e. compare numbers. decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m) -- | <math> leZero :: forall n. SNatI n => LEProof 'Z n -- | <math> leSucc :: LEProof n m -> LEProof ('S n) ('S m) -- | <math> leRefl :: LEProof n n -- | <math> leStep :: LEProof n m -> LEProof n ('S m) -- | <math> leAsym :: LEProof n m -> LEProof m n -> n :~: m -- | <math> leTrans :: LEProof n m -> LEProof m p -> LEProof n p -- | <math> leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n -- | <math> leSwap' :: LEProof n m -> LEProof ('S m) n -> void -- | <math> leStepL :: LEProof ('S n) m -> LEProof n m -- | <math> lePred :: LEProof ('S n) ('S m) -> LEProof n m -- | <math> proofZeroLEZero :: LEProof n 'Z -> n :~: 'Z instance GHC.Show.Show (Data.Type.Nat.LE.ReflStep.LEProof n m) instance GHC.Classes.Eq (Data.Type.Nat.LE.ReflStep.LEProof n m) instance GHC.Classes.Ord (Data.Type.Nat.LE.ReflStep.LEProof n m) instance Control.Category.Category @{Data.Nat.Nat} Data.Type.Nat.LE.ReflStep.LEProof instance (Data.Type.Nat.SNatI n, Data.Type.Nat.SNatI m) => Data.Type.Dec.Decidable (Data.Type.Nat.LE.ReflStep.LEProof n m) -- | Finite numbers. -- -- This module is designed to be imported as -- -- 
--   import Data.Fin (Fin (..))
--   import qualified Data.Fin as Fin
--
module Data.Fin -- | Finite numbers: [0..n-1]. data Fin (n :: Nat) [FZ] :: Fin ('S n) [FS] :: Fin n -> Fin ('S n) -- | Fold Fin. cata :: forall a n. a -> (a -> a) -> Fin n -> a -- | show displaying a structure of Fin. -- -- 
--   >>> explicitShow (0 :: Fin N.Nat1)
--   "FZ"
--
-- -- 
--   >>> explicitShow (2 :: Fin N.Nat3)
--   "FS (FS FZ)"
--
explicitShow :: Fin n -> String -- | showsPrec displaying a structure of Fin. explicitShowsPrec :: Int -> Fin n -> ShowS -- | Convert to Nat. toNat :: Fin n -> Nat -- | Convert from Nat. -- -- 
--   >>> fromNat N.nat1 :: Maybe (Fin N.Nat2)
--   Just 1
--
-- -- 
--   >>> fromNat N.nat1 :: Maybe (Fin N.Nat1)
--   Nothing
--
fromNat :: SNatI n => Nat -> Maybe (Fin n) -- | Convert to Natural. toNatural :: Fin n -> Natural -- | conversion to Integer toInteger :: Integral a => a -> Integer -- | Mirror the values, minBound becomes maxBound, etc. -- -- 
--   >>> map mirror universe :: [Fin N.Nat4]
--   [3,2,1,0]
--
-- -- 
--   >>> reverse universe :: [Fin N.Nat4]
--   [3,2,1,0]
--
mirror :: forall n. SNatI n => Fin n -> Fin n -- | Multiplicative inverse. -- -- Works for Fin n where n is coprime with an -- argument, i.e. in general when n is prime. -- -- 
--   >>> map inverse universe :: [Fin N.Nat5]
--   [0,1,3,2,4]
--
-- -- 
--   >>> zipWith (*) universe (map inverse universe) :: [Fin N.Nat5]
--   [0,1,1,1,1]
--
-- -- Adaptation of pseudo-code in Wikipedia inverse :: forall n. SNatI n => Fin n -> Fin n -- | All values. [minBound .. maxBound] won't work for -- Fin Nat0. -- -- 
--   >>> universe :: [Fin N.Nat3]
--   [0,1,2]
--
universe :: SNatI n => [Fin n] -- | universe which will be fully inlined, if n is known at -- compile time. -- -- 
--   >>> inlineUniverse :: [Fin N.Nat3]
--   [0,1,2]
--
inlineUniverse :: SNatI n => [Fin n] -- | Like universe but NonEmpty. -- -- 
--   >>> universe1 :: NonEmpty (Fin N.Nat3)
--   0 :| [1,2]
--
universe1 :: SNatI n => NonEmpty (Fin ('S n)) -- | 
--   >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3)
--   0 :| [1,2]
--
inlineUniverse1 :: SNatI n => NonEmpty (Fin ('S n)) -- | Fin Nat0 is not inhabited. absurd :: Fin Nat0 -> b -- | Counting to one is boring. -- -- 
--   >>> boring
--   0
--
boring :: Fin Nat1 -- | 
--   >>> map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
--   [0,1,2]
--
weakenLeft :: forall n m. SNatI n => Proxy m -> Fin n -> Fin (Plus n m) -- | 
--   >>> map weakenLeft1 universe :: [Fin N.Nat5]
--   [0,1,2,3]
--
weakenLeft1 :: SNatI n => Fin n -> Fin ('S n) -- | 
--   >>> map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
--   [2,3,4]
--
weakenRight :: forall n m. SNatI n => Proxy n -> Fin m -> Fin (Plus n m) -- | 
--   >>> map weakenRight1 universe :: [Fin N.Nat5]
--   [1,2,3,4]
--
weakenRight1 :: Fin n -> Fin ('S n) -- | Append two Fins together. -- -- 
--   >>> append (Left fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
--   2
--
-- -- 
--   >>> append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
--   7
--
append :: forall n m. SNatI n => Either (Fin n) (Fin m) -> Fin (Plus n m) -- | Inverse of append. -- -- 
--   >>> split fin2 :: Either (Fin N.Nat2) (Fin N.Nat3)
--   Right 0
--
-- -- 
--   >>> split fin1 :: Either (Fin N.Nat2) (Fin N.Nat3)
--   Left 1
--
-- -- 
--   >>> map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)]
--   [Left 0,Left 1,Right 0,Right 1,Right 2]
--
split :: forall n m. SNatI n => Fin (Plus n m) -> Either (Fin n) (Fin m) -- | Return a one less. -- -- 
--   >>> isMin (FZ :: Fin N.Nat1)
--   Nothing
--
-- -- 
--   >>> map isMin universe :: [Maybe (Fin N.Nat3)]
--   [Nothing,Just 0,Just 1,Just 2]
--
isMin :: Fin ('S n) -> Maybe (Fin n) -- | Return a one less. -- -- 
--   >>> isMax (FZ :: Fin N.Nat1)
--   Nothing
--
-- -- 
--   >>> map isMax universe :: [Maybe (Fin N.Nat3)]
--   [Just 0,Just 1,Just 2,Nothing]
--
isMax :: forall n. SNatI n => Fin ('S n) -> Maybe (Fin n) fin0 :: Fin (Plus Nat0 ('S n)) fin1 :: Fin (Plus Nat1 ('S n)) fin2 :: Fin (Plus Nat2 ('S n)) fin3 :: Fin (Plus Nat3 ('S n)) fin4 :: Fin (Plus Nat4 ('S n)) fin5 :: Fin (Plus Nat5 ('S n)) fin6 :: Fin (Plus Nat6 ('S n)) fin7 :: Fin (Plus Nat7 ('S n)) fin8 :: Fin (Plus Nat8 ('S n)) fin9 :: Fin (Plus Nat9 ('S n)) instance GHC.Classes.Eq (Data.Fin.Fin n) instance GHC.Classes.Ord (Data.Fin.Fin n) instance ((n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.S m :: Data.Nat.Nat), Data.Type.Nat.SNatI m) => Test.QuickCheck.Arbitrary.Arbitrary (Data.Fin.Fin n) instance ((n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.S m :: Data.Nat.Nat), Data.Type.Nat.SNatI m) => GHC.Enum.Bounded (Data.Fin.Fin n) instance GHC.Show.Show (Data.Fin.Fin n) instance Data.Type.Nat.SNatI n => GHC.Num.Num (Data.Fin.Fin n) instance Data.Type.Nat.SNatI n => GHC.Real.Real (Data.Fin.Fin n) instance Data.Type.Nat.SNatI n => GHC.Real.Integral (Data.Fin.Fin n) instance Data.Type.Nat.SNatI n => GHC.Enum.Enum (Data.Fin.Fin n) instance Control.DeepSeq.NFData (Data.Fin.Fin n) instance Data.Hashable.Class.Hashable (Data.Fin.Fin n) instance Test.QuickCheck.Arbitrary.CoArbitrary (Data.Fin.Fin n) instance ((n :: Data.Nat.Nat) GHC.Types.~ ('Data.Nat.S m :: Data.Nat.Nat), Data.Type.Nat.SNatI m) => Test.QuickCheck.Function.Function (Data.Fin.Fin n) instance Data.Type.Nat.SNatI n => Data.Universe.Class.Universe (Data.Fin.Fin n) instance Data.Type.Nat.SNatI n => Data.Universe.Class.Finite (Data.Fin.Fin n) -- | This module is designed to be imported qualified: -- -- 
--   import qualified Data.Fin.Enum as E
--
module Data.Fin.Enum -- | Generic enumerations. -- -- Examples: -- -- 
--   >>> from ()
--   0
--
-- -- 
--   >>> to 0 :: ()
--   ()
--
-- -- 
--   >>> to 0 :: Bool
--   False
--
-- -- 
--   >>> map to F.universe :: [Bool]
--   [False,True]
--
-- -- 
--   >>> map (to . (+1) . from) [LT, EQ, GT] :: [Ordering] -- Num Fin is modulo arithmetic
--   [EQ,GT,LT]
--
class Enum a where { -- | The size of an enumeration. type family EnumSize a :: Nat; type EnumSize a = GEnumSize a; } -- | Converts a value to its index. from :: Enum a => a -> Fin (EnumSize a) -- | Converts a value to its index. from :: (Enum a, Generic a, GFrom a, EnumSize a ~ GEnumSize a) => a -> Fin (EnumSize a) -- | Converts from index to the original value. to :: Enum a => Fin (EnumSize a) -> a -- | Converts from index to the original value. to :: (Enum a, Generic a, GTo a, EnumSize a ~ GEnumSize a) => Fin (EnumSize a) -> a -- | Generic version of from. gfrom :: (Generic a, GFrom a) => a -> Fin (GEnumSize a) -- | Constraint for the class that computes gfrom. type GFrom a = GFromRep (Rep a) -- | Generic version of to. gto :: (Generic a, GTo a) => Fin (GEnumSize a) -> a -- | Constraint for the class that computes gto. type GTo a = GToRep (Rep a) -- | Compute the size from the type. type GEnumSize a = EnumSizeRep (Rep a) Nat0 instance Data.Fin.Enum.Enum Data.Void.Void instance Data.Fin.Enum.Enum () instance Data.Fin.Enum.Enum GHC.Types.Bool instance Data.Fin.Enum.Enum GHC.Types.Ordering instance (Data.Fin.Enum.Enum a, Data.Fin.Enum.Enum b, Data.Type.Nat.SNatI (Data.Fin.Enum.EnumSize a)) => Data.Fin.Enum.Enum (Data.Either.Either a b) instance (Data.Fin.Enum.GToRep a, Data.Fin.Enum.GToRep b) => Data.Fin.Enum.GToRep ((GHC.Generics.:+:) @* a b) instance Data.Fin.Enum.GToRep a => Data.Fin.Enum.GToRep (GHC.Generics.M1 @* d c a) instance Data.Fin.Enum.GToRep (GHC.Generics.V1 @*) instance Data.Fin.Enum.GToRep (GHC.Generics.U1 @*) instance (Data.Fin.Enum.GFromRep a, Data.Fin.Enum.GFromRep b) => Data.Fin.Enum.GFromRep ((GHC.Generics.:+:) @* a b) instance Data.Fin.Enum.GFromRep a => Data.Fin.Enum.GFromRep (GHC.Generics.M1 @* d c a) instance Data.Fin.Enum.GFromRep (GHC.Generics.V1 @*) instance Data.Fin.Enum.GFromRep (GHC.Generics.U1 @*)