-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Type-level integers. Like KnownNat, but for integers. -- -- Type-level integers. Like KnownNat, but for integers. @package kind-integer @version 0.4 -- | This module provides a type-level representation for term-level -- Integers. This type-level representation is also named -- Integer, So import this module qualified to avoid name -- conflicts. -- -- 
--   import KindInteger qualified as KI
--
-- -- The implementation details are the same as the ones for type-level -- Naturals in GHC.TypeNats as of base-4.18, and -- it will continue to evolve together with base, trying to -- follow its API as much as possible until the day base -- provides its own type-level integer, making this module redundant. module KindInteger -- | Type-level version of Integer, only ever used as a kind -- for P and N -- -- -- -- NB: Integer is mostly used as a kind, with its types -- constructed using P and N. However, it might also be -- used as type, with its terms constructed using fromPrelude. One -- reason why you may want a Integer at the term-level is so that -- you embed it in larger data-types (for example, the -- KindRational module from the kind-rational -- library embeds this Integer in its Rational type) data Integer -- | type P (x :: Natural) = 'P_ x :: Integer -- | type N (x :: Natural) = 'N_ x :: Integer -- | Make sure zero is represented as P 0, not as -- N 0 -- -- Notice that all the tools in the KindInteger can readily handle -- non-Normalized inputs. This Normalize type-family is -- offered offered only as a convenience in case you want to simplify -- your dealing with zeros. type family Normalize (i :: Integer) :: Integer -- | Convert a term-level KindInteger Integer into a -- term-level Prelude Integer. -- -- 
--   fromPrelude . toPrelude == id
--   toPrelude . fromPrelude == id
--
toPrelude :: Integer -> Integer -- | Obtain a term-level KindInteger Integer from a -- term-level Prelude Integer. This can fail if the -- Prelude Integer is infinite, or if it is so big that it -- would exhaust system resources. -- -- 
--   fromPrelude . toPrelude == id
--   toPrelude . fromPrelude == id
--
-- -- This function can be handy if you are passing KindInteger's -- Integer around for some reason. But, other than this, -- KindInteger doesn't offer any tool to deal with the internals -- of its Integer. fromPrelude :: Integer -> Integer -- | Shows the Integer as it appears literally at the type-level. -- -- This is different from normal show for Integer, which -- shows the term-level value. -- -- 
--   shows            0 (fromPrelude 8) "z" == "8z"
--   showsPrecTypeLit 0 (fromPrelude 8) "z" == "P 8z"
--
showsPrecTypeLit :: Int -> Integer -> ShowS -- | This class gives the integer associated with a type-level integer. -- There are instances of the class for every integer. class KnownInteger (i :: Integer) integerSing :: KnownInteger i => SInteger i -- | Term-level Integer representation of the type-level -- Integer i. integerVal :: forall i proxy. KnownInteger i => proxy i -> Integer -- | This type represents unknown type-level Integer. data SomeInteger SomeInteger :: Proxy n -> SomeInteger -- | Convert a term-level Integer into an unknown type-level -- Integer. someIntegerVal :: Integer -> SomeInteger -- | We either get evidence that this function was instantiated with the -- same type-level Integers, or Nothing. sameInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> Maybe (a :~: b) -- | Singleton type for a type-level Integer i. data SInteger (i :: Integer) -- | A explicitly bidirectional pattern synonym relating an SInteger -- to a KnownInteger constraint. -- -- As an expression: Constructs an explicit SInteger -- i value from an implicit KnownInteger i -- constraint: -- -- 
--   SInteger @i :: KnownInteger i => SInteger i
--
-- -- As a pattern: Matches on an explicit SInteger i -- value bringing an implicit KnownInteger i constraint -- into scope: -- -- 
--   f :: SInteger i -> ..
--   f SInteger = {- SInteger i in scope -}
--
pattern SInteger :: forall i. () => KnownInteger i => SInteger i -- | Return the term-level Prelude Integer number -- corresponding to i in a SInteger i value. fromSInteger :: SInteger i -> Integer -- | Return the term-level KindInteger Integer number -- corresponding to i in a SInteger i value. fromSInteger' :: SInteger i -> Integer -- | Convert a Integer number into an SInteger n -- value, where n is a fresh type-level Integer. withSomeSInteger :: forall rep (r :: TYPE rep). Integer -> (forall n. SInteger n -> r) -> r -- | Convert an explicit SInteger i value into an implicit -- KnownInteger i constraint. withKnownInteger :: forall i rep (r :: TYPE rep). SInteger i -> (KnownInteger i => r) -> r -- | Addition of type-level Integers. type (a :: Integer) + (b :: Integer) = Add_ (Normalize a) (Normalize b) :: Integer infixl 6 + -- | Multiplication of type-level Integers. type (a :: Integer) * (b :: Integer) = Mul_ (Normalize a) (Normalize b) :: Integer infixl 7 * -- | Exponentiation of type-level Integers. -- -- type (a :: Integer) ^ (b :: Integer) = Pow_ (Normalize a) (Normalize b) :: Integer infixr 8 ^ -- | Subtraction of type-level Integers. type (a :: Integer) - (b :: Integer) = a + Negate b :: Integer infixl 6 - -- | Whether a type-level Natural is odd. Zero is not -- considered odd. type Odd (x :: Integer) = Mod (Abs x) 2 ==? 1 :: Bool -- | Whether a type-level Natural is even. Zero is considered -- even. type Even (x :: Integer) = Mod (Abs x) 2 ==? 0 :: Bool -- | Absolute value of a type-level Integer, as a type-level -- Natural. type family Abs (x :: Integer) :: Natural -- | Sign of type-level Integers. -- -- type family Sign (x :: Integer) :: Integer -- | Negation of type-level Integers. type family Negate (x :: Integer) :: Integer -- | Greatest Common Divisor of type-level Integer numbers -- a and b. -- -- Returns a Natural, since the Greatest Common Divisor is always -- positive. type GCD (a :: Integer) (b :: Integer) = NatGCD (Abs a) (Abs b) :: Natural -- | Least Common Multiple of type-level Integer numbers a -- and b. -- -- Returns a Natural, since the Least Common Multiple is always -- positive. type LCM (a :: Integer) (b :: Integer) = NatLCM (Abs a) (Abs b) :: Natural -- | Log base 2 (floored) of type-level Integers. -- -- type Log2 (a :: Integer) = Log2_ (Normalize a) :: Integer -- | Divide of type-level Integer a by b, using -- the specified Rounding r. -- -- type Div (r :: Round) (a :: Integer) (b :: Integer) = Div_ r (Normalize a) (Normalize b) :: Integer infixl 7 `Div` -- | Remainder of the division of type-level Integer -- a by b, using the specified Rounding -- r. -- -- 
--   forall (r :: Round) (a :: Integer) (b :: Integer).
--     (b /= 0) =>
--       Rem r a b  ==  a - b * Div r a b
--
-- -- type Rem (r :: Round) (a :: Integer) (b :: Integer) = a - b * Div r a b :: Integer infixl 7 `Rem` -- | Get both the quotient and the Remainder of the Division -- of type-level Integers a and b using the -- specified Rounding r. -- -- 
--   forall (r :: Round) (a :: Integer) (b :: Integer).
--     (b /= 0) =>
--       DivRem r a b ==  '(Div r a b, Rem r a b)
--
type DivRem (r :: Round) (a :: Integer) (b :: Integer) = '(Div r a b, Rem r a b) :: (Integer, Integer) data Round -- | Round up towards positive infinity. RoundUp :: Round -- | Round down towards negative infinity. Also known as -- Prelude's floor. This is the type of rounding used by -- Prelude's div, mod, divMod, Div, -- Mod. RoundDown :: Round -- | Round towards zero. Also known as Prelude's -- truncate. This is the type of rounding used by Prelude's -- quot, rem, quotRem. RoundZero :: Round -- | Round away from zero. RoundAway :: Round -- | Round towards the closest integer. If halfway between two -- integers, round up towards positive infinity. RoundHalfUp :: Round -- | Round towards the closest integer. If halfway between two -- integers, round down towards negative infinity. RoundHalfDown :: Round -- | Round towards the closest integer. If halfway between two -- integers, round towards zero. RoundHalfZero :: Round -- | Round towards the closest integer. If halfway between two -- integers, round away from zero. RoundHalfAway :: Round -- | Round towards the closest integer. If halfway between two -- integers, round towards the closest even integer. Also known as -- Prelude's round. RoundHalfEven :: Round -- | Round towards the closest integer. If halfway between two -- integers, round towards the closest odd integer. RoundHalfOdd :: Round -- | Divide a by a using the specified Rounding. -- Return the quotient q. See divRem. div :: Round -> Integer -> Integer -> Integer -- | Divide a by a using the specified Rounding. -- Return the remainder m. See divRem. rem :: Round -> Integer -> Integer -> Integer -- | Divide a by a using the specified Rounding. -- Return the quotient q and the remainder m. -- -- 
--   forall (r :: Round) (a :: Integer) (b :: Integer).
--     (b /= 0) =>
--       case divRem r a b of
--         (q, m) -> m == a - b * q
--
divRem :: Round -> Integer -> Integer -> (Integer, Integer) -- | Comparison of type-level Integers, as a function. type CmpInteger (a :: Integer) (b :: Integer) = CmpInteger_ (Normalize a) (Normalize b) :: Ordering -- | Like sameInteger, but if the type-level Integers aren't -- equal, this additionally provides proof of LT or GT. cmpInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> OrderingI a b -- | Whether the internal representation of the Integers are equal. -- -- Note that this is not the same as (==). Use (==) unless -- you know what you are doing. eqIntegerRep :: Integer -> Integer -> Bool -- | This should be exported by Data.Type.Ord. type (a :: k) ==? (b :: k) = OrdCond (Compare a b) 'False 'True 'False :: Bool infixr 4 ==? -- | This should be exported by Data.Type.Ord. type (a :: k) == (b :: k) = (a ==? b) ~ 'True :: Constraint infixr 4 == -- | This should be exported by Data.Type.Ord. type (a :: k) /=? (b :: k) = OrdCond (Compare a b) 'True 'False 'True :: Bool infixr 4 /=? -- | This should be exported by Data.Type.Ord. type (a :: k) /= (b :: k) = (a /=? b) ~ 'True :: Constraint infixr 4 /= instance GHC.Enum.Bounded KindInteger.Round instance GHC.Enum.Enum KindInteger.Round instance GHC.Read.Read KindInteger.Round instance GHC.Show.Show KindInteger.Round instance GHC.Classes.Ord KindInteger.Round instance GHC.Classes.Eq KindInteger.Round instance GHC.Classes.Eq KindInteger.SomeInteger instance GHC.Classes.Ord KindInteger.SomeInteger instance GHC.Show.Show KindInteger.SomeInteger instance GHC.Read.Read KindInteger.SomeInteger instance GHC.TypeNats.KnownNat x => KindInteger.KnownInteger (KindInteger.P x) instance GHC.TypeNats.KnownNat x => KindInteger.KnownInteger (KindInteger.N x) instance GHC.Show.Show (KindInteger.SInteger i) instance Data.Type.Equality.TestEquality KindInteger.SInteger instance Data.Type.Coercion.TestCoercion KindInteger.SInteger instance Data.Singletons.Decide.SDecide KindInteger.Integer instance GHC.Classes.Eq KindInteger.Integer instance GHC.Classes.Ord KindInteger.Integer instance GHC.Show.Show KindInteger.Integer instance GHC.Read.Read KindInteger.Integer