type-level-0.2.4: Type-level programming library

Portabilitynon-portable (MPTC, non-standard instances)
Stabilityexperimental
Maintaineralfonso.acosta@gmail.com

Data.TypeLevel.Num.Ops

Contents

Description

Type-level numerical operations and its value-level reflection functions.

Synopsis

Successor/Predecessor

class (Nat x, Pos y) => Succ x y | x -> y, y -> xSource

Successor type-level relation. Succ x y establishes that succ x = y.

succ :: Succ x y => x -> ySource

value-level reflection function for the Succ type-level relation

class (Pos x, Nat y) => Pred x y | x -> y, y -> xSource

Predecessor type-level relation. Pred x y establishes that pred x = y.

pred :: Pred x y => x -> ySource

value-level reflection function for the Pred type-level relation

Addition/Subtraction

class (Add' x y z, Add' y x z) => Add x y z | x y -> z, z x -> y, z y -> xSource

Addition type-level relation. Add x y z establishes that x + y = z.

(+) :: Add x y z => x -> y -> zSource

value-level reflection function for the Add type-level relation

class Sub x y z | x y -> z, z x -> y, z y -> xSource

Subtraction type-level relation. Sub x y z establishes that x - y = z

(-) :: Sub x y z => x -> y -> zSource

value-level reflection function for the Sub type-level relation

Multiplication/Division

class (Nat x, Nat y, Nat z) => Mul x y z | x y -> zSource

Multiplication type-level relation. Mul x y z establishes that x * y = z. Note it isn't relational (i.e. its inverse cannot be used for division, however, even if it could, the resulting division would only work for zero-remainder divisions)

(*) :: Mul x y z => x -> y -> zSource

value-level reflection function for the multiplication type-level relation

class Div x y z | x y -> z, x z -> y, y z -> xSource

Division type-level relation. Remainder-discarding version of DivMod. Note it is not relational (due to DivMod not being relational)

div :: Div x y z => x -> y -> zSource

value-level reflection function for the Div type-level relation

class Mod x y r | x y -> rSource

Remainder of division, type-level relation. Mod x y r establishes that r is the reminder of dividing x by y.

mod :: Mod x y r => x -> y -> rSource

value-level reflection function for the Mod type-level relation

class (Nat x, Pos y) => DivMod x y q r | x y -> q rSource

Division and Remainder type-level relation. DivMod x y q r establishes that xy = q + ry Note it is not relational (i.e. its inverse cannot be used for multiplication).

divMod :: DivMod x y q r => x -> y -> (q, r)Source

value-level reflection function for the DivMod type-level relation

class (Pos d, Nat x) => IsDivBy d x Source

Is-divisible-by type-level assertion. e.g IsDivBy d x establishes that x is divisible by d.

isDivBy :: IsDivBy d x => d -> xSource

value-level reflection function for IsDivBy

Special efficiency cases

class (Nat x, Nat q) => Mul10 x q | x -> q, q -> xSource

Multiplication by 10 type-level relation (based on DivMod10). Mul10 x y establishes that 10 * x = y.

mul10 :: Mul10 x q => x -> qSource

value-level reflection function for Mul10

class (Nat x, Nat q) => Div10 x q | x -> q, q -> xSource

Division by 10 type-level relation (based on DivMod10)

div10 :: Div10 x q => x -> qSource

value-level reflection function for Mul10

class (Nat i, Nat x) => DivMod10 x i l | i l -> x, x -> i lSource

Division by 10 and Remainer type-level relation (similar to DivMod).

This operation is much faster than DivMod. Furthermore, it is the general, non-structural, constructor/deconstructor since it splits a decimal numeral into its initial digits and last digit. Thus, it allows to inspect the structure of a number and is normally used to create type-level operations.

Note that contrary to DivMod, DivMod10 is relational (it can be used to multiply by 10)

divMod10 :: DivMod10 x q r => x -> (q, r)Source

value-level reflection function for DivMod10

Exponientiation/Logarithm

class (Nat b, Nat e, Nat r) => ExpBase b e r | b e -> rSource

Exponentation type-level relation. ExpBase b e r establishes that b^e = r Note it is not relational (i.e. it cannot be used to express logarithms)

(^) :: ExpBase b e r => b -> e -> rSource

value-level reflection function for the ExpBase type-level relation

class (Pos b, b :>=: D2, Pos x, Nat e) => LogBase b x e | b x -> eSource

logBase :: LogBaseF b x e f => b -> x -> eSource

value-level reflection function for LogBase

class (Pos b, b :>=: D2, Pos x, Nat e, Bool f) => LogBaseF b x e f | b x -> e fSource

Version of LogBase which also outputs if the logarithm calculated was exact. f indicates if the resulting logarithm has no fractional part (i.e. tells if the result provided is exact)

logBaseF :: LogBaseF b x e f => b -> x -> (e, f)Source

value-level reflection function for LogBaseF

class (Pos b, b :>=: D2, Pos x) => IsPowOf b x Source

Assert that a number (x) can be expressed as the power of another one (b) (i.e. the fractional part of log_base_b x = 0, or, in a different way, exists y . b^y = x).

isPowOf :: IsPowOf b x => b -> x -> ()Source

Special efficiency cases

class (Nat x, Pos y) => Exp10 x y | x -> y, y -> xSource

Base-10 Exponentiation type-level relation

exp10 :: Exp10 x y => x -> ySource

value-level reflection function for Exp10

class (Pos x, Nat y) => Log10 x y | x -> ySource

Base-10 logarithm type-level relation Note it is not relational (cannot be used to express Exponentation to 10) However, it works with any positive numeral (not just powers of 10)

log10 :: Log10 x y => x -> ySource

value-level reflection function for Log10

Comparison assertions

General comparison assertion

class (Nat x, Nat y) => Trich x y r | x y -> rSource

Trichotomy type-level relation. 'Trich x y r' establishes the relation (r) between x and y. The obtained relation (r) Can be LT (if x is lower than y), EQ (if x equals y) or GT (if x is greater than y)

trich :: Trich x y r => z -> x -> rSource

value-level reflection function for the comparison type-level assertion

Type-level values denoting comparison results

data LT Source

Lower than

data EQ Source

Equal

data GT Source

Greater than

Abbreviated comparison assertions

class x :==: y Source

Equality abbreviated type-level assertion

class x :>: y Source

Greater-than abbreviated type-level assertion

class x :<: y Source

Lower-than abbreviated type-level assertion

class x :>=: y Source

Greater-than or equal abbreviated type-level assertion

class x :<=: y Source

Lower-than or equal abbreviated type-level assertion

(==) :: x :==: y => x -> y -> ()Source

value-level reflection function for the equality abbreviated type-level assertion

(>) :: x :>: y => x -> y -> ()Source

value-level reflection function for the equality abbreviated type-level assertion

(<) :: x :<: y => x -> y -> ()Source

value-level reflection function for the lower-than abbreviated type-level assertion

(>=) :: x :>=: y => x -> y -> ()Source

value-level reflection function for the greater-than or equal abbreviated type-level assertion

(<=) :: x :<=: y => x -> y -> ()Source

value-level reflection function for the lower-than or equal abbreviated type-level assertion

Maximum/Minimum

class Max x y z | x y -> zSource

Maximum type-level relation

max :: Max x y z => x -> y -> zSource

value-level reflection function for the maximum type-level relation

class Min x y z | x y -> zSource

Minimum type-level relation

min :: Min x y z => x -> y -> zSource

value-level reflection function for the minimum type-level relation

Greatest Common Divisor

class (Nat x, Nat y, Nat gcd) => GCD x y gcd | x y -> gcdSource

Greatest Common Divisor type-level relation

gcd :: GCD x y z => x -> y -> zSource

value-level reflection function for the GCD type-level relation