Kinds.Integer

Type-level Integer.

Import Integer qualified as K and refer to it as K.Integer.

It turns out this is approximately identical to an in-progress GHC change https://github.com/ghc-proposals/ghc-proposals/pull/154, right down to the particulars of how to encode kind-classes. Apparently I was on the right track! TODO(awpr): when that thing is merged and readily available, remove this or turn it into a compat package.

Once that proposal is complete, we can migrate by replacing K.Integer with just Integer.

Type-level Integers

data Integer

Type-level signed numbers

Constructors

Pos Nat

Neg Nat

Instances

type ToInteger (n :: Integer)

Defined in Kinds.Integer

type ToInteger (n :: Integer) = n

type FromNat n

Defined in Kinds.Integer

type FromNat n = 'Pos n

type Compare (x :: Integer) (y :: Integer)

Defined in Kinds.Integer

type Compare (x :: Integer) (y :: Integer) = CmpInteger x y

type (x :: Integer) * (y :: Integer)

Defined in Kinds.Integer

type (x :: Integer) * (y :: Integer) = MulInteger x y

type (x :: Integer) - (y :: Integer)

Defined in Kinds.Integer

type (x :: Integer) - (y :: Integer) = SubInteger x y

type (x :: Integer) + (y :: Integer)

Defined in Kinds.Integer

type (x :: Integer) + (y :: Integer) = AddInteger x y

type family ToInteger (n :: k) :: Integer

Type-level conversion to Integer. Like toInteger in Integral.

Instances

type ToInteger (n :: Nat)

Defined in Kinds.Num

type ToInteger (n :: Nat) = 'Pos n

type ToInteger (n :: Integer)

Defined in Kinds.Integer

type ToInteger (n :: Integer) = n

Runtime Values

class KnownInteger (n :: Integer) where

Mostly internal; the "snumber" package provides more useful functionality.

Methods

integerVal :: Integer

Instances

KnownNat n => KnownInteger ('Pos n)

Defined in Kinds.Integer

Methods

integerVal :: Integer

KnownNat n => KnownInteger ('Neg n)

Defined in Kinds.Integer

Methods

integerVal :: Integer

Specialized Arithmetic and Comparison

type family AddInteger m n where ...

Addition of type-level integers.

Equations

AddInteger ('Pos m) ('Pos n) = 'Pos (m + n)

AddInteger ('Pos m) ('Neg n) = m -# n

AddInteger ('Neg m) ('Pos n) = n -# m

AddInteger ('Neg m) ('Neg n) = 'Neg (m + n)

type family SubInteger m n where ...

Subtraction of type-level integers.

Equations

SubInteger ('Pos m) ('Pos n) = m -# n

SubInteger ('Pos m) ('Neg n) = 'Pos (m + n)

SubInteger ('Neg m) ('Pos n) = 'Neg (m + n)

SubInteger ('Neg m) ('Neg n) = n -# m

type family CmpInteger m n where ...

Comparison of type-level integers.

Equations

CmpInteger ('Pos m) ('Pos n) = Compare m n

CmpInteger ('Pos 0) ('Neg 0) = 'EQ

CmpInteger ('Pos m) ('Neg n) = 'GT

CmpInteger ('Neg 0) ('Pos 0) = 'EQ

CmpInteger ('Neg m) ('Pos n) = 'LT

CmpInteger ('Neg m) ('Neg n) = Compare n m

type family MulInteger m n where ...

Multiplication of type-level integers.

Equations

MulInteger ('Pos m) ('Pos n) = 'Pos (m * n)

MulInteger ('Pos m) ('Neg n) = 0 -# (m * n)

MulInteger ('Neg m) ('Pos n) = 0 -# (m * n)

MulInteger ('Neg m) ('Neg n) = 'Pos (m * n)

type family (m :: Nat) -# (n :: Nat) where ...

Given two Nats m and n, computes m - n as an Integer.

Equations

n -# 0 = 'Pos n

0 -# n = 'Neg n

m -# n = OrdCond (Compare m n) ('Neg (n - m)) ('Pos 0) ('Pos (m - n))

Axioms

plusMinusInverseL :: ((m + n) -# m) :~: 'Pos n

Subtracting the left summand gives back the right summand.

plusMinusInverseR :: ((m + n) -# n) :~: 'Pos m

Subtracting the right summand gives back the left summand.

mulCommutes :: MulInteger m n :~: MulInteger n m

Multiplication of integers is commutative.