Portability | non-portable (MPTC, non-standard instances) |
---|---|
Stability | experimental |
Maintainer | alfonso.acosta@gmail.com |
Data.TypeLevel.Num.Ops
Contents
Description
Type-level numerical operations and its value-level reflection functions.
- 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
.
class (Pos x, Nat y) => Pred x y | x -> y, y -> xSource
Predecessor type-level relation. Pred x y
establishes
that pred x = y
.
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
.
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
.
class (Nat x, Nat q) => Div10 x q | x -> q, q -> xSource
Division by 10 type-level relation (based on DivMod10)
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)
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, 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)
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
).
Special efficiency cases
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)
Comparison assertions
General comparison assertion
trich :: Trich x y r => z -> x -> rSource
value-level reflection function for the comparison type-level assertion
Type-level values denoting comparison results
Abbreviated comparison assertions
(==) :: 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
max :: Max x y z => x -> y -> zSource
value-level reflection function for the maximum type-level relation
min :: Min x y z => x -> y -> zSource
value-level reflection function for the minimum type-level relation