Portability | non-portable (MPTC, non-standard instances) |
---|---|
Stability | experimental |
Maintainer | alfonso.acosta@gmail.com |
Type-level numerical operations and its value-level reflection functions.
- type family Succ n
- succ :: x -> Succ x
- type family Pred n
- pred :: x -> Pred x
- type family Add m n :: *
- (+) :: x -> y -> Add x y
- type family Sub x y
- (-) :: x -> y -> Sub x y
- type family Mul m n
- (*) :: x -> y -> Mul x y
- type family Div x y
- div :: x -> y -> Div x y
- type family Mod x y
- mod :: x -> y -> Mod x y
- class (Pos d, Nat x) => IsDivBy d x
- isDivBy :: IsDivBy d x => d -> x -> ()
- type family Mul10 n
- mul10 :: x -> Mul10 x
- type family Div10 m
- div10 :: x -> Div10 x
- type family DivMod10 n
- divMod10 :: x -> (Div10 x, Mod10 x)
- type family ExpBase b e
- (^) :: b -> e -> ExpBase b e
- type family Exp10 x
- exp10 :: x -> Exp10 x
- type family Log10 x
- log10 :: x -> Log10 x
- type family Trich x y
- trich :: x -> y -> Trich x y
- data LT
- data EQ
- data GT
- type family OrderingEq o1 o2
- type family NatEq x y
- type family x :>: y
- type family x :<: y
- type family x :>=: y
- type family x :<=: y
- (>) :: x -> y -> x :>: y
- (<) :: x -> y -> x :<: y
- (>=) :: x -> y -> x :>=: y
- (<=) :: x -> y -> x :<=: y
- type family Max x y
- max :: x -> y -> Max x y
- type family Min x y
- min :: x -> y -> Min x y
- type family GCD x y
- gcd :: x -> y -> GCD x y
Successor/Predecessor
Successor type-level relation. Succ x y
establishes
that succ x = y
.
Assoc notes: Cannot avoid malformed types
Addition/Subtraction
Multiplication/Division
(*) :: x -> y -> Mul x ySource
value-level reflection function for the multiplication 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
Multiplication by 10 type-level relation (based on DivMod10
).
Mul10 x y
establishes that 10 * x = y
.
Exponientiation/Logarithm
(^) :: b -> e -> ExpBase b eSource
value-level reflection function for the ExpBase type-level relation
Special efficiency cases
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
).
class (Pos b, b :>=: D2, Pos x) => IsPowOf b x instance (Trich x b cmp, IsPowOf' b x cmp) => IsPowOf b x class (Pos b, b :>=: D2, Pos x) => IsPowOf' b x cmp
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 :: x -> y -> Trich x ySource
value-level reflection function for the comparison type-level assertion
Type-level values denoting comparison results
type family OrderingEq o1 o2 Source