|
Data.TypeLevel.Num.Ops | Portability | non-portable (MPTC, non-standard instances) | Stability | experimental | Maintainer | alfonso.acosta@gmail.com |
|
|
|
|
|
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
|
|
|
Successor type-level relation. Succ x y establishes
that succ x = y.
|
|
|
|
value-level reflection function for the Succ type-level relation
|
|
|
Predecessor type-level relation. Pred x y establishes
that pred x = y.
|
|
|
|
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 -> x | Source |
|
Addition type-level relation. Add x y z establishes
that x + y = z.
|
|
|
|
value-level reflection function for the Add type-level relation
|
|
class Sub x y z | x y -> z, z x -> y, z y -> x | Source |
|
Subtraction type-level relation. Sub x y z establishes
that x - y = z
|
|
|
|
value-level reflection function for the Sub type-level relation
|
|
Multiplication/Division
|
|
|
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)
|
|
|
|
value-level reflection function for the multiplication type-level relation
|
|
class Div x y z | x y -> z, x z -> y, y z -> x | Source |
|
Division type-level relation. Remainder-discarding version of DivMod.
Note it is not relational (due to DivMod not being relational)
|
|
|
|
value-level reflection function for the Div type-level relation
|
|
class Mod x y r | x y -> r | Source |
|
Remainder of division, type-level relation. Mod x y r establishes that
r is the reminder of dividing x by y.
|
|
|
|
value-level reflection function for the Mod type-level relation
|
|
|
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).
|
|
|
|
value-level reflection function for the DivMod type-level relation
|
|
|
Is-divisible-by type-level assertion. e.g IsDivBy d x establishes that
x is divisible by d.
|
|
|
|
value-level reflection function for IsDivBy
|
|
Special efficiency cases
|
|
|
Multiplication by 10 type-level relation (based on DivMod10).
Mul10 x y establishes that 10 * x = y.
|
|
|
|
value-level reflection function for Mul10
|
|
|
Division by 10 type-level relation (based on DivMod10)
|
|
|
|
value-level reflection function for Mul10
|
|
class (Nat i, Nat x) => DivMod10 x i l | i l -> x, x -> i l | Source |
|
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)
|
|
|
|
value-level reflection function for DivMod10
|
|
Exponientiation/Logarithm
|
|
|
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)
|
|
|
|
value-level reflection function for the ExpBase type-level relation
|
|
|
|
|
|
value-level reflection function for LogBase
|
|
|
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)
|
|
|
|
value-level reflection function for LogBaseF
|
|
|
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).
|
|
|
|
|
Special efficiency cases
|
|
|
Base-10 Exponentiation type-level relation
|
|
|
|
value-level reflection function for Exp10
|
|
|
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)
|
|
|
|
value-level reflection function for Log10
|
|
Comparison assertions
|
|
General comparison assertion
|
|
|
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)
|
|
|
|
value-level reflection function for the comparison type-level assertion
|
|
Type-level values denoting comparison results
|
|
|
|
|
|
|
|
|
|
|
Abbreviated comparison assertions
|
|
|
Equality abbreviated type-level assertion
|
|
|
|
Greater-than abbreviated type-level assertion
|
|
|
|
Lower-than abbreviated type-level assertion
|
|
|
|
Greater-than or equal abbreviated type-level assertion
|
|
|
|
Lower-than or equal abbreviated type-level assertion
|
|
|
|
value-level reflection function for the equality abbreviated
type-level assertion
|
|
|
value-level reflection function for the equality abbreviated
type-level assertion
|
|
|
value-level reflection function for the lower-than abbreviated
type-level assertion
|
|
|
value-level reflection function for the greater-than or equal abbreviated
type-level assertion
|
|
|
value-level reflection function for the lower-than or equal abbreviated
type-level assertion
|
|
Maximum/Minimum
|
|
class Max x y z | x y -> z | Source |
|
Maximum type-level relation
|
|
|
|
value-level reflection function for the maximum type-level relation
|
|
class Min x y z | x y -> z | Source |
|
Minimum type-level relation
|
|
|
|
value-level reflection function for the minimum type-level relation
|
|
Greatest Common Divisor
|
|
|
Greatest Common Divisor type-level relation
|
|
|
|
value-level reflection function for the GCD type-level relation
|
|
Produced by Haddock version 2.6.1 |