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)

• A positive number +x is represented as P x.
• Zero can be represented as P 0 (see notes at 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).

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.

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

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

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.

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"

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

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

This type represents unknown type-level Integer.

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

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

Singleton type for a type-level Integer 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 -}

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

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

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

Addition of type-level Integers.

Multiplication of type-level Integers.

Exponentiation of type-level Integers.

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

Subtraction of type-level Integers.

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

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

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

Sign of type-level Integers.

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

Negation of type-level Integers.

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

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

Least Common Multiple of type-level Integer numbers a and b.

Returns a Natural, since the Least Common Multiple is always positive.

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

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

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

• Division by zero doesn't type-check.

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.

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)

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

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

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

Comparison of type-level Integers, as a function.

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

This should be exported by Data.Type.Ord.

This should be exported by Data.Type.Ord.

This should be exported by Data.Type.Ord.

This should be exported by Data.Type.Ord.