Safe Haskell	None
Language	Haskell2010

Kinds.Integer

Contents

Type-level Integers
- Runtime Values
- Specialized Arithmetic and Comparison
Axioms

Description

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.

Synopsis

data Integer
- = Pos Nat
- | Neg Nat
type family ToInteger (n :: k) :: Integer
class KnownInteger (n :: Integer) where
- integerVal :: Integer
type family AddInteger m n where ...
type family SubInteger m n where ...
type family CmpInteger m n where ...
type family MulInteger m n where ...
type family (m :: Nat) -# (n :: Nat) where ...
plusMinusInverseL :: ((m + n) -# m) :~: 'Pos n
plusMinusInverseR :: ((m + n) -# n) :~: 'Pos m
mulCommutes :: MulInteger m n :~: MulInteger n m

Type-level Integers

data Integer Source #

Type-level signed numbers

Constructors

Pos Nat
Neg Nat

Instances

Instances details

type ToInteger (n :: Integer) Source #
Instance details Defined in Kinds.Integer type ToInteger (n :: Integer) = n
type FromNat n Source #
Instance details Defined in Kinds.Integer type FromNat n = 'Pos n
type Compare (x :: Integer) (y :: Integer) Source #
Instance details Defined in Kinds.Integer type Compare (x :: Integer) (y :: Integer) = CmpInteger x y
type (x :: Integer) * (y :: Integer) Source #
Instance details Defined in Kinds.Integer type (x :: Integer) * (y :: Integer) = MulInteger x y
type (x :: Integer) - (y :: Integer) Source #
Instance details Defined in Kinds.Integer type (x :: Integer) - (y :: Integer) = SubInteger x y
type (x :: Integer) + (y :: Integer) Source #
Instance details Defined in Kinds.Integer type (x :: Integer) + (y :: Integer) = AddInteger x y

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

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

Instances

Instances details

type ToInteger (n :: Nat) Source #
Instance details Defined in Kinds.Num type ToInteger (n :: Nat) = 'Pos n
type ToInteger (n :: Integer) Source #
Instance details Defined in Kinds.Integer type ToInteger (n :: Integer) = n

Runtime Values

class KnownInteger (n :: Integer) where Source #

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

Methods

integerVal :: Integer Source #

Instances

Instances details

KnownNat n => KnownInteger ('Pos n) Source #
Instance details Defined in Kinds.Integer Methods integerVal :: Integer Source #
KnownNat n => KnownInteger ('Neg n) Source #
Instance details Defined in Kinds.Integer Methods integerVal :: Integer Source #

Specialized Arithmetic and Comparison

type family AddInteger m n where ... Source #

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

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

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

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

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 Source #

Subtracting the left summand gives back the right summand.

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

Subtracting the right summand gives back the left summand.

mulCommutes :: MulInteger m n :~: MulInteger n m Source #

Multiplication of integers is commutative.