| Copyright | (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch and KTH's SAM group |
|---|---|
| License | BSD-style (see the file LICENSE) |
| Maintainer | alfonso.acosta@gmail.com |
| Stability | experimental |
| Portability | non-portable (MPTC, non-standard instances) |
| Safe Haskell | None |
| Language | Haskell98 |
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
- 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
- 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 -> x Source
Successor type-level relation. Succ x y establishes
that succ x = y.
class (Pos x, Nat y) => Pred x y | x -> y, y -> x Source
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 -> x Source
Addition type-level relation. Add x y z establishes
that x + y = z.
(+) :: Add x y z => x -> y -> z infixl 6 Source
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
(-) :: Sub x y z => x -> y -> z infixl 6 Source
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 -> z Source
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' Source | |
| (Add z y z', Mul D7 y z) => Mul D8 y z' Source | |
| (Add z y z', Mul D6 y z) => Mul D7 y z' Source | |
| (Add z y z', Mul D5 y z) => Mul D6 y z' Source | |
| (Add z y z', Mul D4 y z) => Mul D5 y z' Source | |
| (Add z y z', Mul D3 y z) => Mul D4 y z' Source | |
| (Add z y z', Mul D2 y z) => Mul D3 y z' Source | |
| Add y y z => Mul D2 y z Source | |
| Nat y => Mul D1 y y Source | |
| Nat y => Mul D0 y D0 Source | |
| (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' Source |
(*) :: Mul x y z => x -> y -> z infixl 7 Source
value-level reflection function for the multiplication type-level relation
class Div x y z | x y -> z Source
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 -> z infixl 7 Source
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.
mod :: Mod x y r => x -> y -> r infixl 7 Source
value-level reflection function for the Mod type-level relation
class (Nat x, Pos y) => DivMod x y q r | x y -> q r Source
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 -> x Source
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 Source
Division by 10 type-level relation (based on DivMod10)
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
| DivMod10 D9 D0 D9 Source | |
| DivMod10 D8 D0 D8 Source | |
| DivMod10 D7 D0 D7 Source | |
| DivMod10 D6 D0 D6 Source | |
| DivMod10 D5 D0 D5 Source | |
| DivMod10 D4 D0 D4 Source | |
| DivMod10 D3 D0 D3 Source | |
| DivMod10 D2 D0 D2 Source | |
| DivMod10 D1 D0 D1 Source | |
| DivMod10 D0 D0 D0 Source | |
| Nat ((:*) D9 l) => DivMod10 ((:*) D9 l) D9 l Source | |
| Nat ((:*) D8 l) => DivMod10 ((:*) D8 l) D8 l Source | |
| Nat ((:*) D7 l) => DivMod10 ((:*) D7 l) D7 l Source | |
| Nat ((:*) D6 l) => DivMod10 ((:*) D6 l) D6 l Source | |
| Nat ((:*) D5 l) => DivMod10 ((:*) D5 l) D5 l Source | |
| Nat ((:*) D4 l) => DivMod10 ((:*) D4 l) D4 l Source | |
| Nat ((:*) D3 l) => DivMod10 ((:*) D3 l) D3 l Source | |
| Nat ((:*) D2 l) => DivMod10 ((:*) D2 l) D2 l Source | |
| Nat ((:*) D1 l) => DivMod10 ((:*) D1 l) D1 l Source | |
| (Nat ((:*) x l), Nat ((:*) ((:*) x l) l')) => DivMod10 ((:*) ((:*) x l) l') ((:*) x l) l' Source |
Exponientiation/Logarithm
class (Nat b, Nat e, Nat r) => ExpBase b e r | b e -> r Source
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' Source | |
| (Mul r b r', ExpBase b D7 r) => ExpBase b D8 r' Source | |
| (Mul r b r', ExpBase b D6 r) => ExpBase b D7 r' Source | |
| (Mul r b r', ExpBase b D5 r) => ExpBase b D6 r' Source | |
| (Mul r b r', ExpBase b D4 r) => ExpBase b D5 r' Source | |
| (Mul r b r', ExpBase b D3 r) => ExpBase b D4 r' Source | |
| (Mul r b r', ExpBase b D2 r) => ExpBase b D3 r' Source | |
| Mul b b r => ExpBase b D2 r Source | |
| Nat b => ExpBase b D1 b Source | |
| Nat b => ExpBase b D0 D1 Source | |
| (Nat b, Pos ((:*) ei el), Nat r, Mul b r r', Pred ((:*) ei el) e', ExpBase b e' r) => ExpBase b ((:*) ei el) r' Source |
(^) :: ExpBase b e r => b -> e -> r infixr 8 Source
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 f Source
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 (Nat x, Pos y) => Exp10 x y | x -> y, y -> x Source
Base-10 Exponentiation type-level relation
Instances
| Exp10 D0 D1 Source | |
| Exp10 D9 ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) D0) D0) D0) D0) Source | |
| Exp10 D8 ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) D0) D0) D0) Source | |
| Exp10 D7 ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) D0) D0) Source | |
| Exp10 D6 ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) D0) Source | |
| Exp10 D5 ((:*) ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) D0) Source | |
| Exp10 D4 ((:*) ((:*) ((:*) ((:*) D1 D0) D0) D0) D0) Source | |
| Exp10 D3 ((:*) ((:*) ((:*) D1 D0) D0) D0) Source | |
| Exp10 D2 ((:*) ((:*) D1 D0) D0) Source | |
| Exp10 D1 ((:*) D1 D0) Source | |
| (Pred ((:*) xi xl) x', Exp10 x' ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) y D0) D0) D0) D0) D0) D0) D0) D0) D0)) => Exp10 ((:*) xi xl) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) ((:*) y D0) D0) D0) D0) D0) D0) D0) D0) D0) D0) Source |
class (Pos x, Nat y) => Log10 x y | x -> y Source
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
class (Nat x, Nat y) => Trich x y r | x y -> r Source
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
trich :: Trich x y r => z -> x -> r Source
value-level reflection function for the comparison type-level assertion
Type-level values denoting comparison results
Lower than
Instances
Equal
Greater than
Instances
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
(==) :: x :==: y => x -> y -> () infix 4 Source
value-level reflection function for the equality abbreviated type-level assertion
(>) :: x :>: y => x -> y -> () infix 4 Source
value-level reflection function for the equality abbreviated type-level assertion
(<) :: x :<: y => x -> y -> () infix 4 Source
value-level reflection function for the lower-than abbreviated type-level assertion
(>=) :: x :>=: y => x -> y -> () infix 4 Source
value-level reflection function for the greater-than or equal abbreviated type-level assertion
(<=) :: x :<=: y => x -> y -> () infix 4 Source
value-level reflection function for the lower-than or equal abbreviated type-level assertion
Maximum/Minimum
max :: Max x y z => x -> y -> z Source
value-level reflection function for the maximum type-level relation
min :: Min x y z => x -> y -> z Source
value-level reflection function for the minimum type-level relation