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 (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 Cmp (x :: Integer) (y :: Integer)

Defined in Kinds.Integer

type Cmp (x :: Integer) (y :: Integer) = CmpInteger 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) = Cmp 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) = Cmp 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 = CaseOrdering (Cmp 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.

Utility

type family CaseOrdering (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) :: k where ...

Type-level eliminator for Ordering.

CaseOrdering o lt eq gt selects from among lt, eq, and gt according to o. This is primarily exported so Haddock doesn't complain about being unable to link it when it's mentioned in type instance clauses.

Equations

CaseOrdering 'LT lt eq gt = lt

CaseOrdering 'EQ lt eq gt = eq

CaseOrdering 'GT lt eq gt = gt