|
| 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)
| |  Instances | | Nat y => Mul D0 y D0 | | Nat y => Mul D1 y y | | Add y y z => Mul D2 y z | | (Add z y z', Mul D2 y z) => Mul D3 y z' | | (Add z y z', Mul D3 y z) => Mul D4 y z' | | (Add z y z', Mul D4 y z) => Mul D5 y z' | | (Add z y z', Mul D5 y z) => Mul D6 y z' | | (Add z y z', Mul D6 y z) => Mul D7 y z' | | (Add z y z', Mul D7 y z) => Mul D8 y z' | | (Add z y z', Mul D8 y z) => Mul D9 y z' | | (Pos (xi :* xl), Nat y, Mul xi y z, Mul10 z z10, Mul xl y dy, Add dy z10 z') => Mul (xi :* xl) y z' |
|
|
|
|
| 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)
| | | Instances | |
|
|
|
| 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)
| | | Instances | | (Mul r b r', ExpBase b D8 r) => ExpBase b D9 r' | | (Mul r b r', ExpBase b D7 r) => ExpBase b D8 r' | | (Mul r b r', ExpBase b D6 r) => ExpBase b D7 r' | | (Mul r b r', ExpBase b D5 r) => ExpBase b D6 r' | | (Mul r b r', ExpBase b D4 r) => ExpBase b D5 r' | | (Mul r b r', ExpBase b D3 r) => ExpBase b D4 r' | | (Mul r b r', ExpBase b D2 r) => ExpBase b D3 r' | | Mul b b r => ExpBase b D2 r | | Nat b => ExpBase b D1 b | | Nat b => ExpBase b D0 D1 | | Nat b => ExpBase b D0 D1 | | (Nat b, Pos (ei :* el), Nat r, Mul b r r', Pred (ei :* el) e', ExpBase b e' r) => ExpBase b (ei :* el) r' |
|
|
|
|
| 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
| | | Instances | |
|
|
|
| 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)
| | | Instances | |
|
|
|
| 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)
| | | Instances | |
|
