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

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.

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)

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) = 'Positive 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) = 'Negative 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

Linking type and value level

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.

integerVal' :: forall i. 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.

Singleton values

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 type-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 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 Div (a :: Integer) (b :: Integer) = Div_ (Normalize a) (Normalize b) :: Integer infixl 7

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 Mod (a :: Integer) (b :: Integer) = (Div a b * Negate b) + a :: Integer infixl 7

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 Quot (a :: Integer) (b :: Integer) = Quot_ (Normalize a) (Normalize b) :: Integer infixl 7

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 Rem (a :: Integer) (b :: Integer) = (Quot a b * Negate b) + a :: Integer infixl 7

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

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.

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.