|
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.
| | Instances | |
|
|
|
value-level reflection function for the Succ type-level relation
|
|
|
Predecessor type-level relation. Pred x y establishes
that pred x = y.
| | Instances | |
|
|
|
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.
| | Instances | (Add' x y z, Add' y x z) => Add 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
| | Instances | |
|
|
|
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 | (Add z y z', Mul D8 y z) => Mul D9 y z' | (Add z y z', Mul D7 y z) => Mul D8 y z' | (Add z y z', Mul D6 y z) => Mul D7 y z' | (Add z y z', Mul D5 y z) => Mul D6 y z' | (Add z y z', Mul D4 y z) => Mul D5 y z' | (Add z y z', Mul D3 y z) => Mul D4 y z' | (Add z y z', Mul D2 y z) => Mul D3 y z' | Add y y z => Mul D2 y z | Nat y => Mul D1 y y | Nat y => Mul D0 y D0 | (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)
| | Instances | |
|
|
|
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.
| | Instances | |
|
|
|
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).
| | Instances | |
|
|
|
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.
| | Instances | |
|
|
|
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.
| | Instances | |
|
|
|
value-level reflection function for Mul10
|
|
|
Division by 10 type-level relation (based on DivMod10)
| | Instances | |
|
|
|
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, 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
|
|
|
| Instances | |
|
|
|
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)
| | Instances | |
|
|
|
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).
| | Instances | |
|
|
|
|
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 | |
|
|
|
value-level reflection function for the comparison type-level assertion
|
|
Type-level values denoting comparison results
|
|
|
Lower than
| Instances | |
|
|
|
Equal
| Instances | |
|
|
|
Greater than
| Instances | CS GT r GT | Trich D9 D8 GT | Trich D9 D7 GT | Trich D9 D6 GT | Trich D9 D5 GT | Trich D9 D4 GT | Trich D9 D3 GT | Trich D9 D2 GT | Trich D9 D1 GT | Trich D9 D0 GT | Trich D8 D7 GT | Trich D8 D6 GT | Trich D8 D5 GT | Trich D8 D4 GT | Trich D8 D3 GT | Trich D8 D2 GT | Trich D8 D1 GT | Trich D8 D0 GT | Trich D7 D6 GT | Trich D7 D5 GT | Trich D7 D4 GT | Trich D7 D3 GT | Trich D7 D2 GT | Trich D7 D1 GT | Trich D7 D0 GT | Trich D6 D5 GT | Trich D6 D4 GT | Trich D6 D3 GT | Trich D6 D2 GT | Trich D6 D1 GT | Trich D6 D0 GT | Trich D5 D4 GT | Trich D5 D3 GT | Trich D5 D2 GT | Trich D5 D1 GT | Trich D5 D0 GT | Trich D4 D3 GT | Trich D4 D2 GT | Trich D4 D1 GT | Trich D4 D0 GT | Trich D3 D2 GT | Trich D3 D1 GT | Trich D3 D0 GT | Trich D2 D1 GT | Trich D2 D0 GT | Trich D1 D0 GT | (Pos b, b :>=: D2, Pos x, DivMod x b q D0, IsPowOf b q) => IsPowOf' b x GT | Max' x y GT x | (Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCD' x y False GT gcd | (Pos b, b :>=: D2, Pos x, DivMod x b q r, IsZero r rz, And rz f' f, Pred e e', LogBaseF b q e' f') => LogBaseF' b x e f GT | (Nat x, Pos y, Sub x y x', Pred q q', DivMod x' y q' r) => DivMod' x y q r GT | Pos (:* yi yl) => Trich (:* yi yl) D9 GT | Pos (:* yi yl) => Trich (:* yi yl) D8 GT | Pos (:* yi yl) => Trich (:* yi yl) D7 GT | Pos (:* yi yl) => Trich (:* yi yl) D6 GT | Pos (:* yi yl) => Trich (:* yi yl) D5 GT | Pos (:* yi yl) => Trich (:* yi yl) D4 GT | Pos (:* yi yl) => Trich (:* yi yl) D3 GT | Pos (:* yi yl) => Trich (:* yi yl) D2 GT | Pos (:* yi yl) => Trich (:* yi yl) D1 GT | Pos (:* yi yl) => Trich (:* yi yl) D0 GT |
|
|
|
Abbreviated comparison assertions
|
|
|
Equality abbreviated type-level assertion
| | Instances | |
|
|
|
Greater-than abbreviated type-level assertion
| | Instances | |
|
|
|
Lower-than abbreviated type-level assertion
| | Instances | |
|
|
|
Greater-than or equal abbreviated type-level assertion
| | Instances | |
|
|
|
Lower-than or equal abbreviated type-level assertion
| | Instances | |
|
|
|
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
| | Instances | (Max' x y b z, Trich x y b) => Max x y z |
|
|
|
|
value-level reflection function for the maximum type-level relation
|
|
class Min x y z | x y -> z | Source |
|
Minimum type-level relation
| | Instances | (Max' y x b z, Trich x y b) => Min x y z |
|
|
|
|
value-level reflection function for the minimum type-level relation
|
|
Greatest Common Divisor
|
|
|
Greatest Common Divisor type-level relation
| | Instances | (Nat x, Nat y, Trich x y cmp, IsZero y yz, GCD' x y yz cmp gcd) => GCD x y gcd |
|
|
|
|
value-level reflection function for the GCD type-level relation
|
|
Produced by Haddock version 2.6.1 |