type-level-0.2.4: Type-level programming librarySource codeContentsIndex
Data.TypeLevel.Num.Ops
Portabilitynon-portable (MPTC, non-standard instances)
Stabilityexperimental
Maintaineralfonso.acosta@gmail.com
Contents
Successor/Predecessor
Addition/Subtraction
Multiplication/Division
Special efficiency cases
Exponientiation/Logarithm
Special efficiency cases
Comparison assertions
General comparison assertion
Type-level values denoting comparison results
Abbreviated comparison assertions
Maximum/Minimum
Greatest Common Divisor
Description
Type-level numerical operations and its value-level reflection functions.
Synopsis
class (Nat x, Pos y) => Succ x y | x -> y, y -> x
succ :: Succ x y => x -> y
class (Pos x, Nat y) => Pred x y | x -> y, y -> x
pred :: Pred x y => x -> y
class (Add' x y z, Add' y x z) => Add x y z | x y -> z, z x -> y, z y -> x
(+) :: Add x y z => x -> y -> z
class Sub x y z | x y -> z, z x -> y, z y -> x
(-) :: Sub x y z => x -> y -> z
class (Nat x, Nat y, Nat z) => Mul x y z | x y -> z
(*) :: Mul x y z => x -> y -> z
class Div x y z | x y -> z, x z -> y, y z -> x
div :: Div x y z => x -> y -> z
class Mod x y r | x y -> r
mod :: Mod x y r => x -> y -> r
class (Nat x, Pos y) => DivMod x y q r | x y -> q r
divMod :: DivMod x y q r => x -> y -> (q, r)
class (Pos d, Nat x) => IsDivBy d x
isDivBy :: IsDivBy d x => d -> x
class (Nat x, Nat q) => Mul10 x q | x -> q, q -> x
mul10 :: Mul10 x q => x -> q
class (Nat x, Nat q) => Div10 x q | x -> q, q -> x
div10 :: Div10 x q => x -> q
class (Nat i, Nat x) => DivMod10 x i l | i l -> x, x -> i l
divMod10 :: DivMod10 x q r => x -> (q, r)
class (Nat b, Nat e, Nat r) => ExpBase b e r | b e -> r
(^) :: ExpBase b e r => b -> e -> r
class (Pos b, b :>=: D2, Pos x, Nat e) => LogBase b x e | b x -> e
logBase :: LogBaseF b x e f => b -> x -> e
class (Pos b, b :>=: D2, Pos x, Nat e, Bool f) => LogBaseF b x e f | b x -> e f
logBaseF :: LogBaseF b x e f => b -> x -> (e, f)
class (Pos b, b :>=: D2, Pos x) => IsPowOf b x
isPowOf :: IsPowOf b x => b -> x -> ()
class (Nat x, Pos y) => Exp10 x y | x -> y, y -> x
exp10 :: Exp10 x y => x -> y
class (Pos x, Nat y) => Log10 x y | x -> y
log10 :: Log10 x y => x -> y
class (Nat x, Nat y) => Trich x y r | x y -> r
trich :: Trich x y r => z -> x -> r
data LT
data EQ
data GT
class x :==: y
class x :>: y
class x :<: y
class x :>=: y
class x :<=: y
(==) :: x :==: y => x -> y -> ()
(>) :: x :>: y => x -> y -> ()
(<) :: x :<: y => x -> y -> ()
(>=) :: x :>=: y => x -> y -> ()
(<=) :: x :<=: y => x -> y -> ()
class Max x y z | x y -> z
max :: Max x y z => x -> y -> z
class Min x y z | x y -> z
min :: Min x y z => x -> y -> z
class (Nat x, Nat y, Nat gcd) => GCD x y gcd | x y -> gcd
gcd :: GCD x y z => x -> y -> z
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
Produced by Haddock version 2.6.0