Copyright	Alexey Khudyakov
License	BSD3-style (see LICENSE)
Maintainer	Alexey Khudyakov <alexey.skladnoy@gmail.com>
Stability	unstable
Portability	unportable (GHC only)
Safe Haskell	Safe-Inferred
Language	Haskell2010

TypeLevel.Number.Classes

Contents

Comparison of numbers
Arithmetic operations on numbers
Special classes

Description

This module contain interface type classes for operations with type level numbers.

Synopsis

type family Compare n m :: *
compareN :: n -> m -> Compare n m
data IsLesser
data IsEqual
data IsGreater
class Lesser n m
class LesserEq n m
class Greater n m
class GreaterEq n m
class Positive n
class NonZero n
type family Next n :: *
nextN :: n -> Next n
type family Prev n :: *
prevN :: n -> Prev n
type family Negate n :: *
negateN :: n -> Negate n
type family Add n m :: *
addN :: n -> m -> Add n m
type family Sub n m :: *
subN :: n -> m -> Sub n m
type family Mul n m :: *
mulN :: n -> m -> Mul n m
type family Div n m :: *
divN :: n -> m -> Div n m
type family Normalized n :: *

Comparison of numbers

type family Compare n m :: * Source #

Type family for comparing two numbers. It's expected that for any two valid n and m 'Compare n m' is equal to IsLess when 'n<m', IsEqual when 'n=m' and IsGreater when 'n>m'.

Instances

Instances details

type Compare Z Z Source #
Instance details Defined in TypeLevel.Number.Nat type Compare Z Z = IsEqual
type Compare Z (O n) Source #
Instance details Defined in TypeLevel.Number.Nat type Compare Z (O n) = IsLesser
type Compare Z (I n) Source #
Instance details Defined in TypeLevel.Number.Nat type Compare Z (I n) = IsLesser
type Compare (O n) Z Source #
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) Z = IsGreater
type Compare (I n) Z Source #
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) Z = IsGreater
type Compare (O n) (O m) Source #
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) (O m) = Compare n m
type Compare (O n) (I m) Source #
Instance details Defined in TypeLevel.Number.Nat type Compare (O n) (I m)
type Compare (I n) (I m) Source #
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) (I m) = Compare n m
type Compare (I n) (O m) Source #
Instance details Defined in TypeLevel.Number.Nat type Compare (I n) (O m)

compareN :: n -> m -> Compare n m Source #

Data labels for types comparison

data IsLesser Source #

Instances

Instances details

Show IsLesser Source #
Instance details Defined in TypeLevel.Number.Classes Methods showsPrec :: Int -> IsLesser -> ShowS # show :: IsLesser -> String # showList :: [IsLesser] -> ShowS #

data IsEqual Source #

Instances

Instances details

Show IsEqual Source #
Instance details Defined in TypeLevel.Number.Classes Methods showsPrec :: Int -> IsEqual -> ShowS # show :: IsEqual -> String # showList :: [IsEqual] -> ShowS #

data IsGreater Source #

Instances

Instances details

Show IsGreater Source #
Instance details Defined in TypeLevel.Number.Classes Methods showsPrec :: Int -> IsGreater -> ShowS # show :: IsGreater -> String # showList :: [IsGreater] -> ShowS #

Specialized type classes

These type classes are meant to be used in contexts to ensure relations between numbers. For example:

someFunction :: Lesser n m => Data n -> Data m -> Data n
someFunction = ...

They have generic instances and every number which is instance of Compare type family is instance of these type classes.

These instance could have problems. They weren't exensively tested. Also error messages are really unhelpful.

class Lesser n m Source #

Numbers n and m are instances of this class if and only is n < m.

Instances

Instances details

Compare n m ~ IsLesser => Lesser n m Source #
Instance details Defined in TypeLevel.Number.Classes

class LesserEq n m Source #

Numbers n and m are instances of this class if and only is n <= m.

Instances

Instances details

OneOfTwo (Compare n m) IsLesser IsEqual => LesserEq n m Source #
Instance details Defined in TypeLevel.Number.Classes

class Greater n m Source #

Numbers n and m are instances of this class if and only is n > m.

Instances

Instances details

Compare n m ~ IsGreater => Greater n m Source #
Instance details Defined in TypeLevel.Number.Classes

class GreaterEq n m Source #

Numbers n and m are instances of this class if and only is n >= m.

Instances

Instances details

OneOfTwo (Compare n m) IsGreater IsEqual => GreaterEq n m Source #
Instance details Defined in TypeLevel.Number.Classes

Special traits

class Positive n Source #

Positive number.

Instances

Instances details

Nat (O n) => Positive (O n) Source #
Instance details Defined in TypeLevel.Number.Nat
Nat (I n) => Positive (I n) Source #
Instance details Defined in TypeLevel.Number.Nat

class NonZero n Source #

Non-zero number. For naturals it's same as positive

Instances

Instances details

Nat (O n) => NonZero (O n) Source #
Instance details Defined in TypeLevel.Number.Nat
Nat (I n) => NonZero (I n) Source #
Instance details Defined in TypeLevel.Number.Nat

Arithmetic operations on numbers

type family Next n :: * Source #

Next number.

Instances

Instances details

type Next ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Next ZZ = D1 ZZ
type Next Z Source #
Instance details Defined in TypeLevel.Number.Nat type Next Z = I Z
type Next (D1 n) Source #
Instance details Defined in TypeLevel.Number.Int type Next (D1 n) = Normalized (Dn (Next n))
type Next (D0 n) Source #
Instance details Defined in TypeLevel.Number.Int type Next (D0 n) = D1 n
type Next (Dn n) Source #
Instance details Defined in TypeLevel.Number.Int type Next (Dn n) = Normalized (D0 n)
type Next (O n) Source #
Instance details Defined in TypeLevel.Number.Nat type Next (O n) = I n
type Next (I n) Source #
Instance details Defined in TypeLevel.Number.Nat type Next (I n) = O (Next n)

nextN :: n -> Next n Source #

type family Prev n :: * Source #

Previous number

Instances

Instances details

type Prev ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Prev ZZ = Dn ZZ
type Prev (D1 n) Source #
Instance details Defined in TypeLevel.Number.Int type Prev (D1 n) = Normalized (D0 n)
type Prev (D0 n) Source #
Instance details Defined in TypeLevel.Number.Int type Prev (D0 n) = Dn n
type Prev (Dn n) Source #
Instance details Defined in TypeLevel.Number.Int type Prev (Dn n) = Normalized (D1 (Prev n))
type Prev (O (O n)) Source #
Instance details Defined in TypeLevel.Number.Nat type Prev (O (O n)) = I (Prev (O n))
type Prev (O (I n)) Source #
Instance details Defined in TypeLevel.Number.Nat type Prev (O (I n)) = I (Prev (I n))
type Prev (I Z) Source #
Instance details Defined in TypeLevel.Number.Nat type Prev (I Z) = Z
type Prev (I (O n)) Source #
Instance details Defined in TypeLevel.Number.Nat type Prev (I (O n)) = O (O n)
type Prev (I (I n)) Source #
Instance details Defined in TypeLevel.Number.Nat type Prev (I (I n)) = O (I n)

prevN :: n -> Prev n Source #

type family Negate n :: * Source #

Negate number.

Instances

Instances details

type Negate ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Negate ZZ = ZZ
type Negate (D1 n) Source #
Instance details Defined in TypeLevel.Number.Int type Negate (D1 n) = Dn (Negate n)
type Negate (D0 n) Source #
Instance details Defined in TypeLevel.Number.Int type Negate (D0 n) = D0 (Negate n)
type Negate (Dn n) Source #
Instance details Defined in TypeLevel.Number.Int type Negate (Dn n) = D1 (Negate n)

negateN :: n -> Negate n Source #

type family Add n m :: * Source #

Sum of two numbers.

Instances

Instances details

type Add ZZ ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Add ZZ ZZ = ZZ
type Add Z Z Source #
Instance details Defined in TypeLevel.Number.Nat type Add Z Z
type Add ZZ (D1 n) Source #
Instance details Defined in TypeLevel.Number.Int type Add ZZ (D1 n) = Normalized (D1 n)
type Add ZZ (D0 n) Source #
Instance details Defined in TypeLevel.Number.Int type Add ZZ (D0 n) = Normalized (D0 n)
type Add ZZ (Dn n) Source #
Instance details Defined in TypeLevel.Number.Int type Add ZZ (Dn n) = Normalized (Dn n)
type Add Z (O n) Source #
Instance details Defined in TypeLevel.Number.Nat type Add Z (O n)
type Add Z (I n) Source #
Instance details Defined in TypeLevel.Number.Nat type Add Z (I n)
type Add (D1 n) ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Add (D1 n) ZZ = Normalized (D1 n)
type Add (D0 n) ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Add (D0 n) ZZ = Normalized (D0 n)
type Add (Dn n) ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Add (Dn n) ZZ = Normalized (Dn n)
type Add (O n) Z Source #
Instance details Defined in TypeLevel.Number.Nat type Add (O n) Z
type Add (I n) Z Source #
Instance details Defined in TypeLevel.Number.Nat type Add (I n) Z
type Add (D1 n) (D1 m) Source #
Instance details Defined in TypeLevel.Number.Int type Add (D1 n) (D1 m)
type Add (D1 n) (D0 m) Source #
Instance details Defined in TypeLevel.Number.Int type Add (D1 n) (D0 m)
type Add (D1 n) (Dn m) Source #
Instance details Defined in TypeLevel.Number.Int type Add (D1 n) (Dn m)
type Add (D0 n) (D1 m) Source #
Instance details Defined in TypeLevel.Number.Int type Add (D0 n) (D1 m)
type Add (D0 n) (D0 m) Source #
Instance details Defined in TypeLevel.Number.Int type Add (D0 n) (D0 m)
type Add (D0 n) (Dn m) Source #
Instance details Defined in TypeLevel.Number.Int type Add (D0 n) (Dn m)
type Add (Dn n) (D1 m) Source #
Instance details Defined in TypeLevel.Number.Int type Add (Dn n) (D1 m)
type Add (Dn n) (D0 m) Source #
Instance details Defined in TypeLevel.Number.Int type Add (Dn n) (D0 m)
type Add (Dn n) (Dn m) Source #
Instance details Defined in TypeLevel.Number.Int type Add (Dn n) (Dn m)
type Add (O n) (I m) Source #
Instance details Defined in TypeLevel.Number.Nat type Add (O n) (I m)
type Add (O n) (O m) Source #
Instance details Defined in TypeLevel.Number.Nat type Add (O n) (O m)
type Add (I n) (I m) Source #
Instance details Defined in TypeLevel.Number.Nat type Add (I n) (I m)
type Add (I n) (O m) Source #
Instance details Defined in TypeLevel.Number.Nat type Add (I n) (O m)

addN :: n -> m -> Add n m Source #

type family Sub n m :: * Source #

Difference of two numbers.

Instances

Instances details

type Sub ZZ ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Sub ZZ ZZ = ZZ
type Sub Z Z Source #
Instance details Defined in TypeLevel.Number.Nat type Sub Z Z
type Sub ZZ (D1 n) Source #
Instance details Defined in TypeLevel.Number.Int type Sub ZZ (D1 n) = Negate (D1 n)
type Sub ZZ (D0 n) Source #
Instance details Defined in TypeLevel.Number.Int type Sub ZZ (D0 n) = Negate (D0 n)
type Sub ZZ (Dn n) Source #
Instance details Defined in TypeLevel.Number.Int type Sub ZZ (Dn n) = Negate (Dn n)
type Sub (D1 n) ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Sub (D1 n) ZZ = D1 n
type Sub (D0 n) ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Sub (D0 n) ZZ = D0 n
type Sub (Dn n) ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Sub (Dn n) ZZ = Dn n
type Sub (O n) Z Source #
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) Z
type Sub (I n) Z Source #
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) Z
type Sub (D1 n) (D1 m) Source #
Instance details Defined in TypeLevel.Number.Int type Sub (D1 n) (D1 m) = Add (D1 n) (Negate (D1 m))
type Sub (D1 n) (D0 m) Source #
Instance details Defined in TypeLevel.Number.Int type Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))
type Sub (D1 n) (Dn m) Source #
Instance details Defined in TypeLevel.Number.Int type Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))
type Sub (D0 n) (D1 m) Source #
Instance details Defined in TypeLevel.Number.Int type Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))
type Sub (D0 n) (D0 m) Source #
Instance details Defined in TypeLevel.Number.Int type Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m))
type Sub (D0 n) (Dn m) Source #
Instance details Defined in TypeLevel.Number.Int type Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
type Sub (Dn n) (D1 m) Source #
Instance details Defined in TypeLevel.Number.Int type Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))
type Sub (Dn n) (D0 m) Source #
Instance details Defined in TypeLevel.Number.Int type Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))
type Sub (Dn n) (Dn m) Source #
Instance details Defined in TypeLevel.Number.Int type Sub (Dn n) (Dn m) = Add (Dn n) (Negate (Dn m))
type Sub (O n) (I m) Source #
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) (I m)
type Sub (O n) (O m) Source #
Instance details Defined in TypeLevel.Number.Nat type Sub (O n) (O m)
type Sub (I n) (I m) Source #
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) (I m)
type Sub (I n) (O m) Source #
Instance details Defined in TypeLevel.Number.Nat type Sub (I n) (O m)

subN :: n -> m -> Sub n m Source #

type family Mul n m :: * Source #

Product of two numbers.

Instances

Instances details

type Mul n Z Source #
Instance details Defined in TypeLevel.Number.Nat type Mul n Z = Z
type Mul n ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Mul n ZZ = ZZ
type Mul n (O m) Source #
Instance details Defined in TypeLevel.Number.Nat type Mul n (O m) = Normalized (O (Mul n m))
type Mul n (I m) Source #
Instance details Defined in TypeLevel.Number.Nat type Mul n (I m)
type Mul n (D0 m) Source #
Instance details Defined in TypeLevel.Number.Int type Mul n (D0 m) = Normalized (D0 (Mul n m))
type Mul n (D1 m) Source #
Instance details Defined in TypeLevel.Number.Int type Mul n (D1 m)
type Mul n (Dn m) Source #
Instance details Defined in TypeLevel.Number.Int type Mul n (Dn m)

mulN :: n -> m -> Mul n m Source #

type family Div n m :: * Source #

Division of two numbers. n and m should be instances of this class only if remainder of 'n/m' is zero.

divN :: n -> m -> Div n m Source #

Special classes

type family Normalized n :: * Source #

Usually numbers have non-unique representation. This type family is canonical representation of number.

Instances

Instances details

type Normalized ZZ Source #
Instance details Defined in TypeLevel.Number.Int type Normalized ZZ = ZZ
type Normalized Z Source #
Instance details Defined in TypeLevel.Number.Nat type Normalized Z = Z
type Normalized (D1 n) Source #
Instance details Defined in TypeLevel.Number.Int type Normalized (D1 n) = D1 (Normalized n)
type Normalized (D0 n) Source #
Instance details Defined in TypeLevel.Number.Int type Normalized (D0 n)
type Normalized (Dn n) Source #
Instance details Defined in TypeLevel.Number.Int type Normalized (Dn n) = Dn (Normalized n)
type Normalized (O n) Source #
Instance details Defined in TypeLevel.Number.Nat type Normalized (O n)
type Normalized (I n) Source #
Instance details Defined in TypeLevel.Number.Nat type Normalized (I n) = I (Normalized n)