-- 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.1
-- | 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 K
--
--
-- 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
--
--
-- - A positive number +x is represented as P
-- x.
-- - A negative number -x is represented as N
-- x.
-- - Zero can be represented as P 0 or
-- N 0. For consistency, all zero outputs from
-- type families in this KindInteger module use the P
-- 0, but don't assume that this will be the case elsewhere. So, if
-- you need to treat zero specially in some situation, be sure to
-- handle both the P 0 and N 0
-- cases.
--
data Integer
-- |
-- - A positive number +x is represented as P
-- x.
-- - Zero can be represented as P 0 (see notes
-- at Integer).
--
type P (x :: Natural) = 'Positive x :: Integer
-- |
-- - A negative number -x is represented as N
-- x.
-- - Zero can be represented as N 0 (but often
-- isn't, see notes at Integer).
--
type N (x :: Natural) = 'Negative 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
-- | 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
-- | Term-level Integer representation of the type-level
-- Integer i.
integerVal' :: forall i. 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 type-level 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.
--
--
-- - Exponentiation by negative Integer doesn't type-check.
--
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 -
-- | Negation of type-level Integers.
type family Negate (x :: Integer) :: Integer
-- | Division (floored) of type-level Integers.
--
--
-- forall (a :: Integer) (b :: Integer).
-- such that (b /= 0).
-- a == Div a b * Negate b + Mod a b
--
--
--
-- - Division by zero doesn't type-check.
--
type Div (a :: Integer) (b :: Integer) = Div_ (Normalize a) (Normalize b) :: Integer
infixl 7 `Div`
-- | Modulus (floored division) of type-level Integers.
--
--
-- forall (a :: Integer) (b :: Integer).
-- such that (b /= 0).
-- a == Div a b * Negate b + Mod a b
--
--
--
-- - Modulus by zero doesn't type-check.
--
type Mod (a :: Integer) (b :: Integer) = Div a b * Negate b + a :: Integer
infixl 7 `Mod`
-- | Division (truncated) of type-level Integers.
--
--
-- forall (a :: Integer) (b :: Integer).
-- such that (b /= 0).
-- a == Quot a b * Negate b + Rem a b
--
--
--
-- - Division by zero doesn't type-check.
--
type Quot (a :: Integer) (b :: Integer) = Quot_ (Normalize a) (Normalize b) :: Integer
infixl 7 `Quot`
-- | Remainder (truncated division) of type-level Integers.
--
--
-- forall (a :: Integer) (b :: Integer).
-- such that (b /= 0).
-- a == Quot a b * Negate b + Rem a b
--
--
--
-- - Remainder by zero doesn't type-check.
--
type Rem (a :: Integer) (b :: Integer) = Quot a b * Negate b + a :: Integer
infixl 7 `Rem`
-- | Log base 2 (floored) of type-level Integers.
--
--
-- - Logarithm of zero doesn't type-check.
-- - Logarithm of negative number doesn't type-check.
--
type Log2 (a :: Integer) = Log2_ (Normalize a) :: 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
-- | 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.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