KindInteger

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.

Integer kind

data Integer

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.

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)

Instances

Read Integer

Same as Prelude Integer.

Defined in KindInteger

Methods

readsPrec :: Int -> ReadS Integer

readList :: ReadS [Integer]

readPrec :: ReadPrec Integer

readListPrec :: ReadPrec [Integer]

Show Integer

Same as Prelude Integer.

Defined in KindInteger

Methods

showsPrec :: Int -> Integer -> ShowS

show :: Integer -> String

showList :: [Integer] -> ShowS

Eq Integer

Defined in KindInteger

Methods

(==) :: Integer -> Integer -> Bool

(/=) :: Integer -> Integer -> Bool

Ord Integer

Defined in KindInteger

Methods

compare :: Integer -> Integer -> Ordering

(<) :: Integer -> Integer -> Bool

(<=) :: Integer -> Integer -> Bool

(>) :: Integer -> Integer -> Bool

(>=) :: Integer -> Integer -> Bool

max :: Integer -> Integer -> Integer

min :: Integer -> Integer -> Integer

TestCoercion SInteger

Defined in KindInteger

Methods

testCoercion :: forall (a :: k) (b :: k). SInteger a -> SInteger b -> Maybe (Coercion a b)

TestEquality SInteger

Defined in KindInteger

Methods

testEquality :: forall (a :: k) (b :: k). SInteger a -> SInteger b -> Maybe (a :~: b)

type Compare (a :: Integer) (b :: Integer)

Data.Type.Ord support for type-level Integers.

Defined in KindInteger

type Compare (a :: Integer) (b :: Integer) = CmpInteger a b

type P (x :: Natural) = 'P_ x :: Integer

• A positive number +x is represented as P x.
• Zero can be represented as P 0 (see notes at Integer).

type N (x :: Natural) = 'N_ 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 family Normalize (i :: Integer) :: Integer where ...

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.

Equations

Normalize (N 0) = P 0

Normalize i = i

Prelude support

toPrelude :: Integer -> Integer

Convert a term-level KindInteger Integer into a term-level Prelude Integer.

fromPrelude . toPrelude == id
toPrelude . fromPrelude == id

fromPrelude :: 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.

showsPrecTypeLit :: Int -> Integer -> ShowS

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"

Types ⇔ Terms

class KnownInteger (i :: Integer) where

This class gives the integer associated with a type-level integer. There are instances of the class for every integer.

Methods

integerSing :: SInteger i

Instances

KnownNat x => KnownInteger (N x)

Negative numbers and zero.

Defined in KindInteger

Methods

integerSing :: SInteger (N x)

KnownNat x => KnownInteger (P x)

Positive numbers and zero.

Defined in KindInteger

Methods

integerSing :: SInteger (P x)

integerVal :: forall i proxy. KnownInteger i => proxy i -> Integer

Term-level Integer representation of the type-level Integer i.

data SomeInteger

This type represents unknown type-level Integer.

Constructors

forall n.KnownInteger n => SomeInteger (Proxy n)

Instances

Read SomeInteger

Defined in KindInteger

Methods

readsPrec :: Int -> ReadS SomeInteger

readList :: ReadS [SomeInteger]

readPrec :: ReadPrec SomeInteger

readListPrec :: ReadPrec [SomeInteger]

Show SomeInteger

Defined in KindInteger

Methods

showsPrec :: Int -> SomeInteger -> ShowS

show :: SomeInteger -> String

showList :: [SomeInteger] -> ShowS

Eq SomeInteger

Defined in KindInteger

Methods

(==) :: SomeInteger -> SomeInteger -> Bool

(/=) :: SomeInteger -> SomeInteger -> Bool

Ord SomeInteger

Defined in KindInteger

Methods

compare :: SomeInteger -> SomeInteger -> Ordering

(<) :: SomeInteger -> SomeInteger -> Bool

(<=) :: SomeInteger -> SomeInteger -> Bool

(>) :: SomeInteger -> SomeInteger -> Bool

(>=) :: SomeInteger -> SomeInteger -> Bool

max :: SomeInteger -> SomeInteger -> SomeInteger

min :: SomeInteger -> SomeInteger -> SomeInteger

someIntegerVal :: Integer -> SomeInteger

Convert a term-level Integer into an unknown type-level Integer.

sameInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)

We either get evidence that this function was instantiated with the same type-level Integers, or Nothing.

Singletons

data SInteger (i :: Integer)

Singleton type for a type-level Integer i.

Instances

TestCoercion SInteger

Defined in KindInteger

Methods

testCoercion :: forall (a :: k) (b :: k). SInteger a -> SInteger b -> Maybe (Coercion a b)

TestEquality SInteger

Defined in KindInteger

Methods

testEquality :: forall (a :: k) (b :: k). SInteger a -> SInteger b -> Maybe (a :~: b)

Show (SInteger i)

Defined in KindInteger

Methods

showsPrec :: Int -> SInteger i -> ShowS

show :: SInteger i -> String

showList :: [SInteger i] -> ShowS

pattern SInteger :: forall i. () => KnownInteger i => SInteger i

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 -}

fromSInteger :: SInteger i -> Integer

Return the term-level Integer number corresponding to i in a SInteger i value.

withSomeSInteger :: forall rep (r :: TYPE rep). Integer -> (forall n. SInteger n -> r) -> r

Convert a Integer number into an SInteger n value, where n is a fresh type-level Integer.

withKnownInteger :: forall i rep (r :: TYPE rep). SInteger i -> (KnownInteger i => r) -> r

Convert an explicit SInteger i value into an implicit KnownInteger i constraint.

Arithmethic

type (+) (a :: Integer) (b :: Integer) = Add_ (Normalize a) (Normalize b) :: Integer infixl 6

Addition of type-level Integers.

type * (a :: Integer) (b :: Integer) = Mul_ (Normalize a) (Normalize b) :: Integer infixl 7

Multiplication of type-level Integers.

type (^) (a :: Integer) (b :: Integer) = Pow_ (Normalize a) (Normalize b) :: Integer infixr 8

Exponentiation of type-level Integers.

• Exponentiation by negative Integer doesn't type-check.

type (-) (a :: Integer) (b :: Integer) = a + Negate b :: Integer infixl 6

Subtraction of type-level Integers.

type Odd (x :: Integer) = Mod (Abs x) 2 ==? 1 :: Bool

Whether a type-level Natural is odd. Zero is not considered odd.

type Even (x :: Integer) = Mod (Abs x) 2 ==? 0 :: Bool

Whether a type-level Natural is even. Zero is considered even.

type family Abs (x :: Integer) :: Natural where ...

Absolute value of a type-level Integer, as a type-level Natural.

Equations

Abs (P x) = x

Abs (N x) = x

type family Sign (x :: Integer) :: Integer where ...

Sign of type-level Integers.

• P 0 if zero.
• P 1 if positive.
• N 1 if negative.

Equations

Sign (P 0) = P 0

Sign (N 0) = P 0

Sign (P _) = P 1

Sign (N _) = N 1

type family Negate (x :: Integer) :: Integer where ...

Negation of type-level Integers.

Equations

Negate (P 0) = P 0

Negate (P x) = N x

Negate (N x) = P x

type GCD (a :: Integer) (b :: Integer) = NatGCD (Abs a) (Abs b) :: Natural

Greatest Common Divisor of type-level Integer numbers a and b.

Returns a Natural, since the Greatest Common Divisor is always positive.

type LCM (a :: Integer) (b :: Integer) = NatLCM (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 Log2 (a :: Integer) = Log2_ (Normalize a) :: Integer

Log base 2 (floored) of type-level Integers.

• Logarithm of zero doesn't type-check.
• Logarithm of negative number doesn't type-check.

Division

type Div (r :: Round) (a :: Integer) (b :: Integer) = Div_ r (Normalize a) (Normalize b) :: Integer infixl 7

Divide of type-level Integer a by b, using the specified Rounding r.

• Division by zero doesn't type-check.

type Rem (r :: Round) (a :: Integer) (b :: Integer) = a - (b * Div r a b) :: Integer infixl 7

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

• Division by zero doesn't type-check.

type DivRem (r :: Round) (a :: Integer) (b :: Integer) = '(Div r a b, Rem r a b) :: (Integer, Integer)

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)

data Round

Constructors

RoundUp

Round up towards positive infinity.

RoundDown

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.

RoundZero

Round towards zero. Also known as Prelude's truncate. This is the type of rounding used by Prelude's quot, rem, quotRem.

RoundAway

Round away from zero.

RoundHalfUp

Round towards the closest integer. If halfway between two integers, round up towards positive infinity.

RoundHalfDown

Round towards the closest integer. If halfway between two integers, round down towards negative infinity.

RoundHalfZero

Round towards the closest integer. If halfway between two integers, round towards zero.

RoundHalfAway

Round towards the closest integer. If halfway between two integers, round away from zero.

RoundHalfEven

Round towards the closest integer. If halfway between two integers, round towards the closest even integer. Also known as Prelude's round.

RoundHalfOdd

Round towards the closest integer. If halfway between two integers, round towards the closest odd integer.

Instances

Bounded Round

Defined in KindInteger

Methods

minBound :: Round

maxBound :: Round

Enum Round

Defined in KindInteger

Methods

succ :: Round -> Round

pred :: Round -> Round

toEnum :: Int -> Round

fromEnum :: Round -> Int

enumFrom :: Round -> [Round]

enumFromThen :: Round -> Round -> [Round]

enumFromTo :: Round -> Round -> [Round]

enumFromThenTo :: Round -> Round -> Round -> [Round]

Read Round

Defined in KindInteger

Methods

readsPrec :: Int -> ReadS Round

readList :: ReadS [Round]

readPrec :: ReadPrec Round

readListPrec :: ReadPrec [Round]

Show Round

Defined in KindInteger

Methods

showsPrec :: Int -> Round -> ShowS

show :: Round -> String

showList :: [Round] -> ShowS

Eq Round

Defined in KindInteger

Methods

(==) :: Round -> Round -> Bool

(/=) :: Round -> Round -> Bool

Ord Round

Defined in KindInteger

Methods

compare :: Round -> Round -> Ordering

(<) :: Round -> Round -> Bool

(<=) :: Round -> Round -> Bool

(>) :: Round -> Round -> Bool

(>=) :: Round -> Round -> Bool

max :: Round -> Round -> Round

min :: Round -> Round -> Round

Term-level

div

Arguments

:: Round

-> Integer

Dividend a.

-> Integer

Divisor b.

-> Integer

Quotient q.

Divide a by a using the specified Rounding. Return the quotient q. See divRem.

rem

Arguments

:: Round

-> Integer

Dividend a.

-> Integer

Divisor b.

-> Integer

Remainder m.

Divide a by a using the specified Rounding. Return the remainder m. See divRem.

divRem

Arguments

:: Round

-> Integer

Dividend a.

-> Integer

Divisor b.

-> (Integer, Integer)

Quotient q and remainder m.

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

Comparisons

type CmpInteger (a :: Integer) (b :: Integer) = CmpInteger_ (Normalize a) (Normalize b) :: Ordering

Comparison of type-level Integers, as a function.

cmpInteger :: forall a b proxy1 proxy2. (KnownInteger a, KnownInteger b) => proxy1 a -> proxy2 b -> OrderingI a b

Like sameInteger, but if the type-level Integers aren't equal, this additionally provides proof of LT or GT.

Extra

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

This should be exported by Data.Type.Ord.